--- a/src/HOL/UNITY/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <TITLE>HOL/UNITY/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>UNITY--Chandy and Misra's UNITY formalism</H2>
-
-<P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra
-(Addison-Wesley, 1988) presents the UNITY formalism. UNITY consists of an
-abstract programming language of guarded assignments and a calculus for
-reasoning about such programs. Misra's 1994 paper "A Logic for Concurrent
-Programming" presents New UNITY, giving more elegant foundations for a more
-general class of languages. In recent work, Chandy and Sanders have proposed
-new methods for reasoning about systems composed of many components.
-
-<P>This directory formalizes these new ideas for UNITY. The Isabelle examples
-may seem strange to UNITY traditionalists. Hand UNITY proofs tend to be
-written in the forwards direction, as in informal mathematics, while Isabelle
-works best in a backwards (goal-directed) style. Programs are expressed as
-sets of commands, where each command is a relation on states. Quantification
-over commands using [] is easily expressed. At present, there are no examples
-of quantification using ||.
-
-<P>A UNITY assertion denotes the set of programs satisfying it, as
-in the propositions-as-types paradigm. The resulting style is readable if
-unconventional.
-
-<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.
-
-<ADDRESS>
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY></HTML>