*** empty log message ***
authornipkow
Fri Nov 17 13:15:19 1995 +0100 (1995-11-17)
changeset 134071b0a5d83347
parent 1339 f1a3a7b44ff1
child 1341 69fec018854c
*** empty log message ***
src/HOL/IMP/Properties.ML
src/HOL/IMP/README.html
src/HOL/IMP/ROOT.ML
     1.1 --- a/src/HOL/IMP/Properties.ML	Fri Nov 17 12:40:09 1995 +0100
     1.2 +++ b/src/HOL/IMP/Properties.ML	Fri Nov 17 13:15:19 1995 +0100
     1.3 @@ -38,4 +38,4 @@
     1.4  by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
     1.5            dtac bexp_detD, atac, etac (sym RS False_neq_True),
     1.6            fast_tac HOL_cs]);
     1.7 -result();
     1.8 +qed "com_det";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/README.html	Fri Nov 17 13:15:19 1995 +0100
     2.3 @@ -0,0 +1,20 @@
     2.4 +<HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
     2.5 +
     2.6 +<H2>IMP --- A <KBD>while</KBD>-Language and its 3 Semantics</H2>
     2.7 +
     2.8 +The formalization of the denotational, operational and axiomatic semantics of
     2.9 +a simple while-language, including
    2.10 +<UL>
    2.11 +<LI> an equivalence proof between denotational and operational semantics and
    2.12 +<LI> the derivation of the Hoare rules from the denotational semantics.
    2.13 +</UL>
    2.14 +The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
    2.15 +<P>
    2.16 +<KBD>
    2.17 +@book{Winskel,author={Glynn Winskel},
    2.18 +title={The Formal Semantics of Programming Languages},
    2.19 +publisher={MIT Press},year=1993}
    2.20 +</KBD>
    2.21 +<P>
    2.22 +Here is the documentation.
    2.23 +</BODY></HTML>
     3.1 --- a/src/HOL/IMP/ROOT.ML	Fri Nov 17 12:40:09 1995 +0100
     3.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Nov 17 13:15:19 1995 +0100
     3.3 @@ -2,16 +2,6 @@
     3.4      ID:         $Id$
     3.5      Author: 	Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
     3.6      Copyright   1995 TUM
     3.7 -
     3.8 -The formalization of the denotational, operational and axiomatic semantics of
     3.9 -a simple while-language, including
    3.10 -(1) an equivalence proof between denotational and operational semantics and
    3.11 -(2) the derivation of the Hoare rules from the denotational semantics.
    3.12 -The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
    3.13 -
    3.14 -Glynn Winskel. The Formal Semantics of Programming Languages.
    3.15 -MIT Press, 1993.
    3.16 -
    3.17  *)
    3.18  
    3.19  HOL_build_completed;	(*Make examples fail if HOL did*)