--- a/src/CTT/ROOT.ML Sun Dec 30 23:07:31 2007 +0100
+++ b/src/CTT/ROOT.ML Mon Dec 31 19:36:29 2007 +0100
@@ -4,7 +4,5 @@
Copyright 1991 University of Cambridge
*)
-val banner = "Constructive Type Theory";
-writeln banner;
+use_thy "Main";
-use_thy "Main";
--- a/src/FOLP/ROOT.ML Sun Dec 30 23:07:31 2007 +0100
+++ b/src/FOLP/ROOT.ML Mon Dec 31 19:36:29 2007 +0100
@@ -8,7 +8,5 @@
Presence of unknown proof term means that matching does not behave as expected.
*)
-val banner = "First-Order Logic with Natural Deduction with Proof Terms";
-writeln banner;
+use_thy "FOLP";
-use_thy "FOLP";
--- a/src/HOL/TLA/ROOT.ML Sun Dec 30 23:07:31 2007 +0100
+++ b/src/HOL/TLA/ROOT.ML Mon Dec 31 19:36:29 2007 +0100
@@ -4,6 +4,5 @@
Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
*)
-val banner = "Temporal Logic of Actions";
+use_thy "TLA";
-time_use_thy "TLA";
--- 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";
--- a/src/Pure/ROOT.ML Sun Dec 30 23:07:31 2007 +0100
+++ b/src/Pure/ROOT.ML Mon Dec 31 19:36:29 2007 +0100
@@ -4,7 +4,6 @@
Pure Isabelle.
*)
-val banner = "Pure Isabelle";
val version = "Isabelle repository version"; (*filled in automatically!*)
(*if true then some tools will OMIT some proofs*)
--- a/src/ZF/ROOT.ML Sun Dec 30 23:07:31 2007 +0100
+++ b/src/ZF/ROOT.ML Mon Dec 31 19:36:29 2007 +0100
@@ -8,7 +8,5 @@
Paulson.
*)
-val banner = "ZF Set Theory (in FOL)";
-writeln banner;
+use_thy "Main_ZFC";
-use_thy "Main_ZFC";