--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/README.html	Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,36 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<H2>UNITY: Examples Involving Single Programs</H2>
+
+<P> The directory presents verification examples that do not involve program
+composition.  They are mostly taken from Misra's 1994 papers on ``New UNITY'':
+<UL>
+<LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>)
+
+<LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>)
+
+<LI>the communication network
+(<A HREF="Network.thy"><CODE>Network.thy</CODE></A>)
+
+<LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>)
+
+<LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>)
+
+<LI><EM>n</EM>-process deadlock
+(<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>)
+
+<LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>)
+
+<LI>reachability in directed graphs (section 6.4 of the book) (<A
+HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and
+<A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>)
+</UL>
+
+<HR>
+<P>Last modified on $Date$
+
+<ADDRESS>
+<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+</ADDRESS>
+</BODY></HTML>