Old_HOL: ex/ROOT.ML@da00b32c3977 (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";
7949f97df77a Initial revision clasohm parents: diff changeset	15	time_use "ex/meson-test.ML";
9 da00b32c3977 renamed: hol-rec.* to rec., lex-prod. to lexprod., prop-log. to pl.* clasohm parents: 0 diff changeset	16	time_use_thy "ex/lexprod";
0 7949f97df77a Initial revision clasohm parents: diff changeset	17	time_use_thy "ex/puzzle";
7949f97df77a Initial revision clasohm parents: diff changeset	18	time_use "ex/set.ML";
7949f97df77a Initial revision clasohm parents: diff changeset	19	time_use_thy "ex/finite";
9 da00b32c3977 renamed: hol-rec.* to rec., lex-prod. to lexprod., prop-log. to pl.* clasohm parents: 0 diff changeset	20	time_use_thy "ex/pl";
0 7949f97df77a Initial revision clasohm parents: diff changeset	21	time_use_thy "ex/term";
7949f97df77a Initial revision clasohm parents: diff changeset	22	time_use_thy "ex/simult";
7949f97df77a Initial revision clasohm parents: diff changeset	23	maketest "END: Root file for HOL examples";

author	clasohm
	Sun, 17 Oct 1993 17:33:40 +0100
changeset 9	da00b32c3977
parent 0	7949f97df77a
child 14	9b0142dad559
permissions	-rw-r--r--