--- a/auto-proof.rst	Wed Apr 08 21:06:41 2009 +0300
+++ b/auto-proof.rst	Mon Apr 13 18:57:03 2009 +0300
@@ -39,11 +39,29 @@
 
 * IsarMathLib.
 
+The goal of the project is to create a library of formalized mathematics,
+similar to the Mizar Mathematical Library, but written for the Isabelle/Isar
+theorem prover (ZF logic).
+
+See
+
+  http://savannah.nongnu.org/projects/isarmathlib
+  http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel
+
+** http://isarmathlib.org/
+
 This site is an experimental HTML rendering of fragments of the IsarMathLib
 project. IsarMathLib is a library of mathematical proofs formally verified by
 the Isabelle theorem proving environment. The formalization is based on the
 Zermelo-Fraenkel set theory.
 
+** Tiddly Formal Math.
+
+This site is an experimental TiddlyWiki rendering of fragments of the
+IsarMathLib project. IsarMathLib is a library of mathematical proofs formally
+verified by the Isabelle theorem proving environment. The formalization is
+based on the Zermelo-Fraenkel set theory.
+
 See
 
-  http://isarmathlib.org/
+  http://formalmath.tiddlyspot.com/