Old_HOL: IMP/ROOT.ML@a9f7ff3a464c (annotated)

132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	1	(* Title: HOL/IMP/ROOT.ML
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	2	ID: $Id$
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	3	Author: Heiko Loetzbeyer & Robert Sandner, TUM
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	4	Copyright 1994 TUM
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	5
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	6	Executes the formalization of the denotational and operational semantics of a
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	7	simple while-language, including an equivalence proof. The whole development
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	8	essentially formalizes/transcribes chapters 2 and 5 of
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	9
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	10	Glynn Winskel. The Formal Semantics of Programming Languages.
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	11	MIT Press, 1993.
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	12
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	13	*)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	14
132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	15	HOL_build_completed; (Make examples fail if HOL did)
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	16
132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	17	writeln"Root file for HOL/IMP";
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	18	proof_timing := true;
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	19	loadpath := [".","IMP"];
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	20	time_use_thy "Equiv";

author	wenzelm
	Wed, 21 Sep 1994 15:40:41 +0200
changeset 145	a9f7ff3a464c
parent 132	47be9d22a0d6
child 188	32b84b520cd3
permissions	-rw-r--r--