diff -r 4e65a262e821 -r 24f1a6ce1a72 auto-proof.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/auto-proof.rst	Sat Mar 28 18:41:35 2009 +0200
@@ -0,0 +1,49 @@
+-*- outline -*-
+
+* proofgeneral.
+
+  $ sudo apt-get install proofgeneral
+  $ sudo apt-get install proofgeneral-coq
+  $ sudo apt-get install proofgeneral-misc
+  $ sudo apt-get install proofgeneral-doc
+  $ sudo apt-get install proofgeneral-minlog
+
+or build from source:
+
+  $ make clean
+  $ make compile EMACS=xemacs
+  $ cat ~/.emacs
+...
+(load-file "dir/generic/proof-site.el")
+...
+
+See
+
+  http://proofgeneral.inf.ed.ac.uk/
+
+* Isabelle.
+
+Isabelle is a generic proof assistant.
+
+It allows mathematical formulas to be expressed in a formal language and
+provides tools for proving those formulas in a logical calculus. The main
+application is the formalization of mathematical proofs and in particular
+formal verification, which includes proving the correctness of computer
+hardware or software and proving properties of computer languages and
+protocols.
+
+See
+
+  http://isabelle.in.tum.de/overview.html
+  http://en.wikipedia.org/wiki/Isabelle_(theorem_prover)
+
+* IsarMathLib.
+
+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.
+
+See
+
+  http://isarmathlib.org/