src/LCF/ROOT.ML
changeset 25750 4e796867ccb5
parent 17247 6927a62c77dc
child 33615 261abc2e3155
--- a/src/LCF/ROOT.ML	Sun Dec 30 23:07:31 2007 +0100
+++ b/src/LCF/ROOT.ML	Mon Dec 31 19:36:29 2007 +0100
@@ -4,7 +4,5 @@
     Copyright   1992  University of Cambridge
 *)
 
-val banner = "Logic for Computable Functions (in FOL)";
-writeln banner;
+use_thy "LCF";
 
-use_thy "LCF";