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

1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1025 diff changeset	1	(* Title: HOL/IMP/ROOT.ML
924 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	*)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	6
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1025 diff changeset	7	HOL_build_completed; (Make examples fail if HOL did)
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	8
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1025 diff changeset	9	writeln"Root file for HOL/IMP";
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	10	proof_timing := true;
1025 23190112d369 Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 951 diff changeset	11	time_use_thy "Properties";
23190112d369 Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 951 diff changeset	12	time_use_thy "Equiv";
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: 1351 diff changeset	13	time_use_thy "VC";

author	nipkow
	Tue, 23 Jan 1996 10:59:35 +0100
changeset 1447	bc2c0acbbf29
parent 1351	4a960c012383
child 1465	5d7a7e439cec
permissions	-rw-r--r--