isabelle: src/HOL/ex/ROOT.ML@0b268cff9344 (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: HOL/ex/ROOT
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
969 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
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1026 diff changeset	9	HOL_build_completed; (Cause examples to fail if HOL did)
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	10
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1026 diff changeset	11	writeln "Root file for HOL examples";
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	12	proof_timing := true;
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	13
4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	14	(Some examples of recursive function definitions: the TFL package)
4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	15	time_use_thy "Fib";
4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	16	time_use_thy "Primes";
3337 c056d328aa0e Primrec: New example ported from ZF paulson parents: 3294 diff changeset	17	time_use_thy "Primrec";
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	18
4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	19	time_use_thy "NatSum";
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	20	time_use "cla.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	21	time_use "meson.ML";
4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	22	time_use "mesontest.ML";
1719 8b677c7e18bc Now mentions but does not load mesontest2.ML paulson parents: 1639 diff changeset	23	( time_use "mesontest2.ML"; ULTRA SLOW )
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	24	time_use_thy "String";
1174 e57a93d41de0 added mention of new theories BT and Perm lcp parents: 1165 diff changeset	25	time_use_thy "BT";
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	26	time_use_thy "InSort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	27	time_use_thy "Qsort";
f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	28	time_use_thy "Puzzle";
3294 4c73b6508f53 New example: ex/Fib paulson parents: 3243 diff changeset	29
1351 4a960c012383 removed make_chart; clasohm parents: 1296 diff changeset	30	time_use "set.ML";
1026 f2dc38ed53ac ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. nipkow parents: 972 diff changeset	31	time_use_thy "MT";
1296 ae31bb7774a7 added calls of init_html and make_chart clasohm parents: 1174 diff changeset	32
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1026 diff changeset	33	writeln "END: Root file for HOL examples";

author	wenzelm
	Tue, 27 May 1997 15:45:07 +0200
changeset 3362	0b268cff9344
parent 3337	c056d328aa0e
child 3404	91a91790899a
permissions	-rw-r--r--