--- a/src/HOL/README.html Fri Aug 20 15:34:51 1999 +0200
+++ b/src/HOL/README.html Fri Aug 20 15:41:19 1999 +0200
@@ -14,6 +14,21 @@
<DT>Auth
<DD>a new approach to verifying authentication protocols
+<DT>AxClasses
+<DD>a few axiomatic type class examples:
+<DL>
+
+<DT> Tutorial <DD> Some simple axclass demos that go along with the
+<em>axclass</em> Isabelle document (<tt>isatool doc axclass</tt>).
+
+<DT> Group
+<DD> Some bits of group theory.
+
+<DT> Lattice
+<DD> Basic theory of lattices and orders.
+
+</DL>
+
<DT>Hoare
<DD>verification of imperative programs; verification conditions are
generated automatically from pre/post conditions and loop invariants.
@@ -31,6 +46,9 @@
<DT>IOA
<DD>a simple theory of Input/Output Automata
+<DT>Isar_examples
+<DD>some Isabelle/Isar proof documents
+
<DT>Lambda
<DD>a proof of the Church-Rosser theorem for lambda-calculus