# HG changeset patch
# User wenzelm
# Date 1199126189 -3600
# Node ID 4e796867ccb5fabdb8f82f9d42ec4e0322ba9833
# Parent  10e7feb4e595d70fd2c0059b839a8e5fb0ffd2d0
removed obsolete banner;

diff -r 10e7feb4e595 -r 4e796867ccb5 src/CTT/ROOT.ML
--- 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";
diff -r 10e7feb4e595 -r 4e796867ccb5 src/FOLP/ROOT.ML
--- 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";
diff -r 10e7feb4e595 -r 4e796867ccb5 src/HOL/TLA/ROOT.ML
--- 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";
diff -r 10e7feb4e595 -r 4e796867ccb5 src/LCF/ROOT.ML
--- 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";
diff -r 10e7feb4e595 -r 4e796867ccb5 src/Pure/ROOT.ML
--- 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*)
diff -r 10e7feb4e595 -r 4e796867ccb5 src/ZF/ROOT.ML
--- 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";