1.1 --- a/src/HOL/UNITY/README.html	Mon Mar 05 12:31:31 2001 +0100
     1.2 +++ b/src/HOL/UNITY/README.html	Mon Mar 05 15:25:11 2001 +0100
     1.3 @@ -23,32 +23,18 @@
     1.4  in the propositions-as-types paradigm.  The resulting style is readable if
     1.5  unconventional.
     1.6  
     1.7 -<P>
     1.8 -The directory presents a few small examples, mostly taken from Misra's 1994
     1.9 -paper:
    1.10 -<UL>
    1.11 -<LI>common meeting time
    1.12 -
    1.13 -<LI>the token ring
    1.14 -
    1.15 -<LI>the communication network
    1.16 -
    1.17 -<LI>the lift controller (a standard benchmark)
    1.18 -
    1.19 -<LI>a mutual exclusion algorithm
    1.20 -
    1.21 -<LI><EM>n</EM>-process deadlock
    1.22 -
    1.23 -<LI>unordered channel
    1.24 -
    1.25 -<LI>reachability in directed graphs (section 6.4 of the book)
    1.26 -</UL>
    1.27 -
    1.28  <P> Safety proofs (invariants) are often proved automatically.  Progress
    1.29  proofs involving ENSURES can sometimes be proved automatically.  The
    1.30  level of automation appears to be about the same as in HOL-UNITY by Flemming
    1.31  Andersen et al.
    1.32  
    1.33 +<P>
    1.34 +The directory <A HREF="Simple/"><CODE>Simple</CODE></A>
    1.35 +presents a few examples, mostly taken from Misra's 1994
    1.36 +paper, involving single programs.
    1.37 +The directory <A HREF="Comp/"><CODE>Comp</CODE></A>
    1.38 +presents examples of proofs involving program composition.
    1.39 +
    1.40  <HR>
    1.41  <P>Last modified on $Date$
    1.42