removed obsolete banner;
authorwenzelm
Mon Dec 31 19:36:29 2007 +0100 (2007-12-31)
changeset 257504e796867ccb5
parent 25749 10e7feb4e595
child 25751 a4e69ce247e0
removed obsolete banner;
src/CTT/ROOT.ML
src/FOLP/ROOT.ML
src/HOL/TLA/ROOT.ML
src/LCF/ROOT.ML
src/Pure/ROOT.ML
src/ZF/ROOT.ML
     1.1 --- a/src/CTT/ROOT.ML	Sun Dec 30 23:07:31 2007 +0100
     1.2 +++ b/src/CTT/ROOT.ML	Mon Dec 31 19:36:29 2007 +0100
     1.3 @@ -4,7 +4,5 @@
     1.4      Copyright   1991  University of Cambridge
     1.5  *)
     1.6  
     1.7 -val banner = "Constructive Type Theory";
     1.8 -writeln banner;
     1.9 +use_thy "Main";
    1.10  
    1.11 -use_thy "Main";
     2.1 --- a/src/FOLP/ROOT.ML	Sun Dec 30 23:07:31 2007 +0100
     2.2 +++ b/src/FOLP/ROOT.ML	Mon Dec 31 19:36:29 2007 +0100
     2.3 @@ -8,7 +8,5 @@
     2.4  Presence of unknown proof term means that matching does not behave as expected.
     2.5  *)
     2.6  
     2.7 -val banner = "First-Order Logic with Natural Deduction with Proof Terms";
     2.8 -writeln banner;
     2.9 +use_thy "FOLP";
    2.10  
    2.11 -use_thy "FOLP";
     3.1 --- a/src/HOL/TLA/ROOT.ML	Sun Dec 30 23:07:31 2007 +0100
     3.2 +++ b/src/HOL/TLA/ROOT.ML	Mon Dec 31 19:36:29 2007 +0100
     3.3 @@ -4,6 +4,5 @@
     3.4  Adds the Temporal Logic of Actions to a database containing Isabelle/HOL.
     3.5  *)
     3.6  
     3.7 -val banner = "Temporal Logic of Actions";
     3.8 +use_thy "TLA";
     3.9  
    3.10 -time_use_thy "TLA";
     4.1 --- a/src/LCF/ROOT.ML	Sun Dec 30 23:07:31 2007 +0100
     4.2 +++ b/src/LCF/ROOT.ML	Mon Dec 31 19:36:29 2007 +0100
     4.3 @@ -4,7 +4,5 @@
     4.4      Copyright   1992  University of Cambridge
     4.5  *)
     4.6  
     4.7 -val banner = "Logic for Computable Functions (in FOL)";
     4.8 -writeln banner;
     4.9 +use_thy "LCF";
    4.10  
    4.11 -use_thy "LCF";
     5.1 --- a/src/Pure/ROOT.ML	Sun Dec 30 23:07:31 2007 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Mon Dec 31 19:36:29 2007 +0100
     5.3 @@ -4,7 +4,6 @@
     5.4  Pure Isabelle.
     5.5  *)
     5.6  
     5.7 -val banner = "Pure Isabelle";
     5.8  val version = "Isabelle repository version";    (*filled in automatically!*)
     5.9  
    5.10  (*if true then some tools will OMIT some proofs*)
     6.1 --- a/src/ZF/ROOT.ML	Sun Dec 30 23:07:31 2007 +0100
     6.2 +++ b/src/ZF/ROOT.ML	Mon Dec 31 19:36:29 2007 +0100
     6.3 @@ -8,7 +8,5 @@
     6.4  Paulson.
     6.5  *)
     6.6  
     6.7 -val banner = "ZF Set Theory (in FOL)";
     6.8 -writeln banner;
     6.9 +use_thy "Main_ZFC";
    6.10  
    6.11 -use_thy "Main_ZFC";