# HG changeset patch
# User nipkow
# Date 816610519 -3600
# Node ID 71b0a5d8334777bd0cc14dc9ed87ccab4b66f67d
# Parent f1a3a7b44ff13706148d4a93f2aa7bd87323db29
*** empty log message ***
diff -r f1a3a7b44ff1 -r 71b0a5d83347 src/HOL/IMP/Properties.ML
--- 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";
diff -r f1a3a7b44ff1 -r 71b0a5d83347 src/HOL/IMP/README.html
--- /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 @@
+HOL/IMP/ReadMe
+
+IMP --- A while-Language and its 3 Semantics
+
+The formalization of the denotational, operational and axiomatic semantics of
+a simple while-language, including
+
+- an equivalence proof between denotational and operational semantics and
+
- the derivation of the Hoare rules from the denotational semantics.
+
+The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
+
+
+@book{Winskel,author={Glynn Winskel},
+title={The Formal Semantics of Programming Languages},
+publisher={MIT Press},year=1993}
+
+
+Here is the documentation.
+
diff -r f1a3a7b44ff1 -r 71b0a5d83347 src/HOL/IMP/ROOT.ML
--- 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*)