# HG changeset patch
# User wenzelm
# Date 935156479 -7200
# Node ID 96bc013c8987d3e46c39bbe0c354d62f498995f1
# Parent  43a0a5097701228eb1f110c63f2d123b49b0f64c
AxClasses, Isar_examples;

diff -r 43a0a5097701 -r 96bc013c8987 src/HOL/README.html
--- 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