Old_HOL: ex/ROOT.ML@a73f8a7784bd (annotated)

9 da00b32c3977 renamed: hol-rec.* to rec., lex-prod. to lexprod., prop-log. to pl.* clasohm parents: 0 diff changeset	1	(* Title: HOL/ex/ROOT
0 7949f97df77a Initial revision clasohm parents: diff changeset	2	ID: $Id$
7949f97df77a Initial revision clasohm parents: diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
7949f97df77a Initial revision clasohm parents: diff changeset	4	Copyright 1991 University of Cambridge
7949f97df77a Initial revision clasohm parents: diff changeset	5
7949f97df77a Initial revision clasohm parents: diff changeset	6	Executes all examples for Higher-Order Logic.
7949f97df77a Initial revision clasohm parents: diff changeset	7	*)
7949f97df77a Initial revision clasohm parents: diff changeset	8
7949f97df77a Initial revision clasohm parents: diff changeset	9	HOL_build_completed; (Cause examples to fail if HOL did)
7949f97df77a Initial revision clasohm parents: diff changeset	10
7949f97df77a Initial revision clasohm parents: diff changeset	11	writeln"Root file for HOL examples";
7949f97df77a Initial revision clasohm parents: diff changeset	12	proof_timing := true;
46 a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	13	loadpath := ["ex"];
0 7949f97df77a Initial revision clasohm parents: diff changeset	14	time_use "ex/cla.ML";
7949f97df77a Initial revision clasohm parents: diff changeset	15	time_use "ex/meson.ML";
15 25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	16	time_use "ex/mesontest.ML";
46 a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	17	time_use_thy "InSort";
a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	18	time_use_thy "Qsort";
a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	19	time_use_thy "LexProd";
a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	20	time_use_thy "Puzzle";
0 7949f97df77a Initial revision clasohm parents: diff changeset	21	time_use "ex/set.ML";
46 a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	22	time_use_thy "PL";
a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	23	time_use_thy "Term";
a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	24	time_use_thy "Simult";
a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	25	time_use_thy "MT";
0 7949f97df77a Initial revision clasohm parents: diff changeset	26	maketest "END: Root file for HOL examples";

author	nipkow
	Wed, 23 Feb 1994 10:05:35 +0100
changeset 46	a73f8a7784bd
parent 35	c1a3020635a1
child 63	94436622324d
permissions	-rw-r--r--