Old_HOL: ex/ROOT.ML@c789c7441119 (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
222 c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	6	Executes miscellaneous examples for Higher-Order Logic.
0 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
222 c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	11	(writeln"Root file for HOL examples";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	12	proof_timing := true;
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	13	loadpath := ["ex"];
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	14	time_use "ex/cla.ML";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	15	time_use "ex/meson.ML";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	16	time_use "ex/mesontest.ML";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	17	time_use_thy "String";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	18	time_use_thy "InSort";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	19	time_use_thy "Qsort";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	20	time_use_thy "LexProd";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	21	time_use_thy "Puzzle";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	22	time_use_thy "NatSum";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	23	time_use "ex/set.ML";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	24	time_use_thy "SList";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	25	time_use_thy "LList";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	26	time_use_thy "Acc";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	27	time_use_thy "PropLog";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	28	time_use_thy "Term";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	29	time_use_thy "Simult";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	30	time_use_thy "MT";
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	31	writeln "END: Root file for HOL examples"
c789c7441119 No longer calls maketest; instead, the Makefile writes the file lcp parents: 208 diff changeset	32	) handle _ => exit 1;

author	lcp
	Tue, 28 Feb 1995 10:52:55 +0100
changeset 222	c789c7441119
parent 208	deec279dda0a
child 247	05736fb55c13
permissions	-rw-r--r--