isabelle: src/ZF/IMP/ROOT.ML@c05373eebee3 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: ZF/IMP/ROOT.ML
481 ac0568345f88 Initial revision nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1351 diff changeset	3	Author: Heiko Loetzbeyer & Robert Sandner, TUM
481 ac0568345f88 Initial revision nipkow parents: diff changeset	4	Copyright 1994 TUM
ac0568345f88 Initial revision nipkow parents: diff changeset	5
ac0568345f88 Initial revision nipkow parents: diff changeset	6	Executes the formalization of the denotational and operational semantics of a
ac0568345f88 Initial revision nipkow parents: diff changeset	7	simple while-language, including an equivalence proof. The whole development
ac0568345f88 Initial revision nipkow parents: diff changeset	8	essentially formalizes/transcribes chapters 2 and 5 of
ac0568345f88 Initial revision nipkow parents: diff changeset	9
ac0568345f88 Initial revision nipkow parents: diff changeset	10	Glynn Winskel. The Formal Semantics of Programming Languages.
ac0568345f88 Initial revision nipkow parents: diff changeset	11	MIT Press, 1993.
ac0568345f88 Initial revision nipkow parents: diff changeset	12
ac0568345f88 Initial revision nipkow parents: diff changeset	13	*)
ac0568345f88 Initial revision nipkow parents: diff changeset	14
6349 f7750d816c21 removed foo_build_completed -- now handled by session management (via usedir); wenzelm parents: 4446 diff changeset	15	writeln"Root file for ZF/IMP";
481 ac0568345f88 Initial revision nipkow parents: diff changeset	16
4446 097004a470fb tuned; wenzelm parents: 1461 diff changeset	17	set proof_timing;
957 28a48c44ca57 Removed exception handlers, as they are now in ZF/Makefile. lcp parents: 910 diff changeset	18	time_use_thy "Equiv";

author	paulson
	Mon, 02 Aug 1999 11:29:13 +0200
changeset 7145	c05373eebee3
parent 6349	f7750d816c21
child 9000	c20d58286a51
permissions	-rw-r--r--