isabelle: src/HOL/IMP/ROOT.ML@0140ff702b23 (annotated)

924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	1	(* Title: CHOL/IMP/ROOT.ML
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	2	ID: $Id$
936 a6d7b4084761 Hoare logic nipkow parents: 924 diff changeset	3	Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
a6d7b4084761 Hoare logic nipkow parents: 924 diff changeset	4	Copyright 1995 TUM
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	5
936 a6d7b4084761 Hoare logic nipkow parents: 924 diff changeset	6	The formalization of the denotational, operational and axiomatic semantics of
a6d7b4084761 Hoare logic nipkow parents: 924 diff changeset	7	a simple while-language, including
a6d7b4084761 Hoare logic nipkow parents: 924 diff changeset	8	(1) an equivalence proof between denotational and operational semantics and
a6d7b4084761 Hoare logic nipkow parents: 924 diff changeset	9	(2) the derivation of the Hoare rules from the denotational semantics.
a6d7b4084761 Hoare logic nipkow parents: 924 diff changeset	10	The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	11
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	12	Glynn Winskel. The Formal Semantics of Programming Languages.
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	13	MIT Press, 1993.
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	14
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	15	*)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	16
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	17	CHOL_build_completed; (Make examples fail if CHOL did)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	18
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	19	writeln"Root file for CHOL/IMP";
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	20	proof_timing := true;
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	21	loadpath := [".","IMP"];
1025 23190112d369 Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 951 diff changeset	22	time_use_thy "Properties";
23190112d369 Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 951 diff changeset	23	time_use_thy "Equiv";
23190112d369 Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 951 diff changeset	24	time_use_thy "Hoare";

author	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 1025	23190112d369
child 1165	97b2bb5d43c3
permissions	-rw-r--r--