--- a/src/HOL/IMP/Properties.ML Fri Nov 17 12:40:09 1995 +0100
+++ b/src/HOL/IMP/Properties.ML Fri Nov 17 13:15:19 1995 +0100
@@ -38,4 +38,4 @@
by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
dtac bexp_detD, atac, etac (sym RS False_neq_True),
fast_tac HOL_cs]);
-result();
+qed "com_det";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/README.html Fri Nov 17 13:15:19 1995 +0100
@@ -0,0 +1,20 @@
+<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
+
+<H2>IMP --- A <KBD>while</KBD>-Language and its 3 Semantics</H2>
+
+The formalization of the denotational, operational and axiomatic semantics of
+a simple while-language, including
+<UL>
+<LI> an equivalence proof between denotational and operational semantics and
+<LI> the derivation of the Hoare rules from the denotational semantics.
+</UL>
+The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
+<P>
+<KBD>
+@book{Winskel,author={Glynn Winskel},
+title={The Formal Semantics of Programming Languages},
+publisher={MIT Press},year=1993}
+</KBD>
+<P>
+Here is the documentation.
+</BODY></HTML>
--- a/src/HOL/IMP/ROOT.ML Fri Nov 17 12:40:09 1995 +0100
+++ b/src/HOL/IMP/ROOT.ML Fri Nov 17 13:15:19 1995 +0100
@@ -2,16 +2,6 @@
ID: $Id$
Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
Copyright 1995 TUM
-
-The formalization of the denotational, operational and axiomatic semantics of
-a simple while-language, including
-(1) an equivalence proof between denotational and operational semantics and
-(2) the derivation of the Hoare rules from the denotational semantics.
-The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
-
-Glynn Winskel. The Formal Semantics of Programming Languages.
-MIT Press, 1993.
-
*)
HOL_build_completed; (*Make examples fail if HOL did*)