diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/README.html
--- a/src/HOL/UNITY/README.html	Mon Mar 05 12:31:31 2001 +0100
+++ b/src/HOL/UNITY/README.html	Mon Mar 05 15:25:11 2001 +0100
@@ -23,32 +23,18 @@
 in the propositions-as-types paradigm.  The resulting style is readable if
 unconventional.
 
-<P>
-The directory presents a few small examples, mostly taken from Misra's 1994
-paper:
-<UL>
-<LI>common meeting time
-
-<LI>the token ring
-
-<LI>the communication network
-
-<LI>the lift controller (a standard benchmark)
-
-<LI>a mutual exclusion algorithm
-
-<LI><EM>n</EM>-process deadlock
-
-<LI>unordered channel
-
-<LI>reachability in directed graphs (section 6.4 of the book)
-</UL>
-
 <P> Safety proofs (invariants) are often proved automatically.  Progress
 proofs involving ENSURES can sometimes be proved automatically.  The
 level of automation appears to be about the same as in HOL-UNITY by Flemming
 Andersen et al.
 
+<P>
+The directory <A HREF="Simple/"><CODE>Simple</CODE></A>
+presents a few examples, mostly taken from Misra's 1994
+paper, involving single programs.
+The directory <A HREF="Comp/"><CODE>Comp</CODE></A>
+presents examples of proofs involving program composition.
+
 <HR>
 <P>Last modified on $Date$