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

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1352 diff changeset	1	(* Title: LK/ex/ROOT
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1352 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 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	paulson
	Mon, 23 Sep 1996 17:42:56 +0200
changeset 2003	b48f066d52dc
parent 1461	6bcb44e4d6e5
permissions	-rw-r--r--