--- a/auto-proof.rst	Sun Apr 12 22:25:47 2009 +0300
+++ b/auto-proof.rst	Sun Apr 12 22:26:28 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/