--- a/auto-proof.rst	Sat Apr 18 12:46:29 2009 +0300
+++ b/auto-proof.rst	Sat Apr 18 16:09:23 2009 +0300
@@ -73,6 +73,22 @@
 
   http://formalmath.tiddlyspot.com/
 
+* HOL Light.
+
+HOL Light is a computer program to help users prove interesting mathematical
+theorems completely formally in higher order logic. It sets a very exacting
+standard of correctness, but provides a number of automated tools and
+pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and
+real analysis) to save the user work. It is also fully programmable, so users
+can extend it with new theorems and inference rules without compromising its
+soundness.
+
+Ocalm.
+
+See
+
+  http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
+
 * ACL2.
 
 ACL2 (A Computational Logic for Applicative Common Lisp) is a software system
@@ -156,3 +172,12 @@
 
   http://www.ijcar.org/
   http://en.wikipedia.org/wiki/International_Joint_Conference_on_Automated_Reasoning
+
+* Top 100.
+
+  http://www.cs.ru.nl/~freek/100/
+                (winner)
+  http://personal.stevens.edu/~nkahl/Top100Theorems.html
+                (orig list)
+  http://www.cse.unsw.edu.au/~kleing/top100/#5
+                (Isabelle)