isabelle: src/HOL/ex/ROOT.ML@9bf3816298d0 (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
972 e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...) clasohm parents: 970 diff changeset	11	(writeln "Root file for CHOL examples";
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	12	proof_timing := true;
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	13	loadpath := ["ex"];
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	14	time_use "ex/cla.ML";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	15	time_use "ex/meson.ML";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	16	time_use "ex/mesontest.ML";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	17	time_use_thy "String";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	18	time_use_thy "InSort";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	19	time_use_thy "Qsort";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	20	time_use_thy "LexProd";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	21	time_use_thy "Puzzle";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	22	time_use_thy "NatSum";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	23	time_use "ex/set.ML";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	24	time_use_thy "SList";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	25	time_use_thy "LList";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	26	time_use_thy "Acc";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	27	time_use_thy "PropLog";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	28	time_use_thy "Term";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	29	time_use_thy "Simult";
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	30	time_use_thy "MT";
972 e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...) clasohm parents: 970 diff changeset	31	writeln "END: Root file for CHOL examples"
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	32	) handle _ => exit 1;

author	lcp
	Thu, 06 Apr 1995 10:53:21 +0200
changeset 999	9bf3816298d0
parent 972	e61b058d58d2
child 1026	f2dc38ed53ac
permissions	-rw-r--r--