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

970 6d36fe1bb234 fixed bug: HOL_build_completed replaced by CHOL_build_completed clasohm parents: 969 diff changeset	1	(* Title: CHOL/ex/ROOT
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4	Copyright 1991 University of Cambridge
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6	Executes miscellaneous examples for Higher-Order Logic.
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8
970 6d36fe1bb234 fixed bug: HOL_build_completed replaced by CHOL_build_completed clasohm parents: 969 diff changeset	9	CHOL_build_completed; (Cause examples to fail if CHOL did)
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	10
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	11	writeln "Root file for CHOL examples";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	12	proof_timing := true;
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	13	loadpath := ["ex"];
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	14	time_use "ex/cla.ML";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	15	time_use "ex/meson.ML";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	16	time_use "ex/mesontest.ML";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	17	time_use_thy "String";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	18	time_use_thy "InSort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	19	time_use_thy "Qsort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	20	time_use_thy "LexProd";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	21	time_use_thy "Puzzle";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	22	time_use_thy "NatSum";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	23	time_use "ex/set.ML";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	24	time_use_thy "SList";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	25	time_use_thy "LList";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	26	time_use_thy "Acc";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	27	time_use_thy "PropLog";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	28	time_use_thy "Term";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	29	time_use_thy "Simult";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	30	time_use_thy "MT";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	31	writeln "END: Root file for CHOL examples";

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