--- 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$