src/LK/ex/ROOT.ML
changeset 2085 bcc9cbed10b1
parent 2084 5963238bc1b6
child 2086 80ef03e39058
--- a/src/LK/ex/ROOT.ML	Thu Oct 10 10:57:33 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      LK/ex/ROOT
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Executes all examples for Classical Logic. 
-*)
-
-LK_build_completed;    (*Cause examples to fail if LK did*)
-
-writeln"Root file for LK examples";
-
-proof_timing := true;
-time_use "ex/prop.ML";
-time_use "ex/quant.ML";
-time_use "ex/hardquant.ML";
-
-maketest"END: Root file for LK examples";