src/LK/ROOT.ML
changeset 2085 bcc9cbed10b1
parent 2084 5963238bc1b6
child 2086 80ef03e39058
--- a/src/LK/ROOT.ML	Thu Oct 10 10:57:33 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*  Title:      LK/ROOT
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-
-Adds Classical Sequent Calculus to a database containing pure Isabelle. 
-Should be executed in the subdirectory LK.
-*)
-
-val banner = "Classical First-Order Sequent Calculus";
-writeln banner;
-
-init_thy_reader();
-
-print_depth 1;  
-
-use_thy "LK";
-
-use "../Pure/install_pp.ML";
-print_depth 8;
-
-val LK_build_completed = ();    (*indicate successful build*)