isabelle: src/HOL/IMP/ROOT.ML@71b0a5d83347 (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;
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	11	loadpath := [".","IMP"];
1025 23190112d369 Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 951 diff changeset	12	time_use_thy "Properties";
23190112d369 Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 951 diff changeset	13	time_use_thy "Equiv";
23190112d369 Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 951 diff changeset	14	time_use_thy "Hoare";
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1165 diff changeset	15
ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1165 diff changeset	16	make_chart (); (make HTML chart)

author	nipkow
	Fri, 17 Nov 1995 13:15:19 +0100
changeset 1340	71b0a5d83347
parent 1296	ae31bb7774a7
child 1351	4a960c012383
permissions	-rw-r--r--