diff -r 5963238bc1b6 -r bcc9cbed10b1 src/LK/ROOT.ML --- 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*)