Old_HOL: ex/ROOT.ML@c1a3020635a1 (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;
7949f97df77a Initial revision clasohm parents: diff changeset	13	time_use "ex/cla.ML";
7949f97df77a Initial revision clasohm parents: diff changeset	14	time_use "ex/meson.ML";
15 25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	15	time_use "ex/mesontest.ML";
35 c1a3020635a1 added qsort nipkow parents: 15 diff changeset	16	time_use_thy "ex/Qsort";
15 25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	17	time_use_thy "ex/LexProd";
25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	18	time_use_thy "ex/Puzzle";
0 7949f97df77a Initial revision clasohm parents: diff changeset	19	time_use "ex/set.ML";
15 25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	20	time_use_thy "ex/Finite";
25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	21	time_use_thy "ex/PL";
25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	22	time_use_thy "ex/Term";
25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	23	time_use_thy "ex/Simult";
25ec61ee621c renamed meson-test.ML to mesontest.ML, clasohm parents: 14 diff changeset	24	time_use_thy "ex/MT";
0 7949f97df77a Initial revision clasohm parents: diff changeset	25	maketest "END: Root file for HOL examples";

author	nipkow
	Mon, 24 Jan 1994 15:59:44 +0100
changeset 35	c1a3020635a1
parent 15	25ec61ee621c
child 46	a73f8a7784bd
permissions	-rw-r--r--