isabelle: src/LK/ex/ROOT.ML@0140ff702b23 (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: LK/ex/ROOT
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Executes all examples for Classical Logic.
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	LK_build_completed; (Cause examples to fail if LK did)
a5a9c433f639 Initial revision clasohm parents: diff changeset	10
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	writeln"Root file for LK examples";
a5a9c433f639 Initial revision clasohm parents: diff changeset	12
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	proof_timing := true;
a5a9c433f639 Initial revision clasohm parents: diff changeset	14	time_use "ex/prop.ML";
a5a9c433f639 Initial revision clasohm parents: diff changeset	15	time_use "ex/quant.ML";
99 df0cd0fecf86 renamed hard-quant.ML to hardquant.ML clasohm parents: 0 diff changeset	16	time_use "ex/hardquant.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	17
a5a9c433f639 Initial revision clasohm parents: diff changeset	18	maketest"END: Root file for LK examples";

author	lcp
	Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072	0140ff702b23
parent 99	df0cd0fecf86
child 1298	488593372568
permissions	-rw-r--r--