Old_HOL: ex/ROOT.ML@fd1be45b64bf (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";
63 94436622324d Added some sums. nipkow parents: 46 diff changeset	21	time_use_thy "NatSum";
0 7949f97df77a Initial revision clasohm parents: diff changeset	22	time_use "ex/set.ML";
148 13b15899c528 moved LList* to ex nipkow parents: 130 diff changeset	23	time_use_thy "LList";
127 d9527f97246e INSTALLATION OF INDUCTIVE DEFINITIONS lcp parents: 63 diff changeset	24	time_use_thy "Acc";
130 e7dcf3c07865 Updated PL to PropLog using Larrys ind. defs. nipkow parents: 127 diff changeset	25	time_use_thy "PropLog";
46 a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	26	time_use_thy "Term";
a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	27	time_use_thy "Simult";
a73f8a7784bd some more sorting algorithms nipkow parents: 35 diff changeset	28	time_use_thy "MT";
0 7949f97df77a Initial revision clasohm parents: diff changeset	29	maketest "END: Root file for HOL examples";

author	clasohm
	Wed, 02 Nov 1994 11:50:09 +0100
changeset 156	fd1be45b64bf
parent 148	13b15899c528
child 195	df6b3bd14dcb
permissions	-rw-r--r--