removed obsolete init_pps and init_thy_reader;
authorwenzelm
Wed Jul 09 17:00:34 1997 +0200 (1997-07-09)
changeset 3511da4dd8b7ced4
parent 3510 24d235feeb2a
child 3512 9dcb4daa15e8
removed obsolete init_pps and init_thy_reader;
NEWS
src/CTT/ROOT.ML
src/Cube/ROOT.ML
src/FOL/ROOT.ML
src/FOLP/ROOT.ML
src/HOL/Auth/DB-ROOT.ML
src/HOL/ROOT.ML
src/HOL/thy_data.ML
src/HOLCF/ROOT.ML
src/Sequents/ROOT.ML
     1.1 --- a/NEWS	Wed Jul 09 16:54:17 1997 +0200
     1.2 +++ b/NEWS	Wed Jul 09 17:00:34 1997 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  * removed old README and Makefiles;
     1.6  
     1.7 +* removed obsolete init_pps and init_database;
     1.8 +
     1.9  
    1.10  New in Isabelle94-8 (May 1997)
    1.11  ------------------------------
     2.1 --- a/src/CTT/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
     2.2 +++ b/src/CTT/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
     2.3 @@ -12,15 +12,12 @@
     2.4  
     2.5  print_depth 1;  
     2.6  
     2.7 -init_thy_reader();
     2.8 -
     2.9  use_thy "CTT";
    2.10  use "../Provers/typedsimp.ML";
    2.11  use "rew.ML";
    2.12  use_thy "Arith";
    2.13  use_thy "Bool";
    2.14  
    2.15 -init_pps ();
    2.16  print_depth 8;
    2.17  
    2.18  val CTT_build_completed = ();   (*indicate successful build*)
     3.1 --- a/src/Cube/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
     3.2 +++ b/src/Cube/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
     3.3 @@ -1,20 +1,18 @@
     3.4 -(*  Title:      Cube/ROOT
     3.5 +(*  Title:      Cube/ROOT.ML
     3.6      ID:         $Id$
     3.7      Author:     Tobias Nipkow
     3.8      Copyright   1992  University of Cambridge
     3.9  
    3.10 -The Lambda-Cube a la Barendregt
    3.11 +The Lambda-Cube a la Barendregt.
    3.12  *)
    3.13  
    3.14  val banner = "Barendregt's Lambda-Cube";
    3.15  writeln banner;
    3.16  
    3.17 -init_thy_reader();
    3.18 +print_depth 1;  
    3.19  
    3.20 -print_depth 1;  
    3.21  use_thy "Cube";
    3.22  
    3.23 -init_pps ();
    3.24  print_depth 8;
    3.25  
    3.26  val Cube_build_completed = ();  (*indicate successful build*)
     4.1 --- a/src/FOL/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
     4.2 +++ b/src/FOL/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
     4.3 @@ -11,8 +11,6 @@
     4.4  
     4.5  writeln banner;
     4.6  
     4.7 -init_thy_reader();
     4.8 -
     4.9  print_depth 1;  
    4.10  
    4.11  use "../Provers/splitter.ML";
    4.12 @@ -49,7 +47,6 @@
    4.13   (fn _ => [ (deepen_tac FOL_cs 0 1) ]);
    4.14  
    4.15  
    4.16 -init_pps ();
    4.17  print_depth 8;
    4.18  
    4.19  val FOL_build_completed = ();   (*indicate successful build*)
     5.1 --- a/src/FOLP/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
     5.2 +++ b/src/FOLP/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
     5.3 @@ -12,9 +12,8 @@
     5.4  
     5.5  writeln banner;
     5.6  
     5.7 -init_thy_reader();
     5.8 +print_depth 1;
     5.9  
    5.10 -print_depth 1;  
    5.11  use_thy "IFOLP";
    5.12  use_thy "FOLP";
    5.13  
    5.14 @@ -75,7 +74,7 @@
    5.15  
    5.16  use "simpdata.ML";
    5.17  
    5.18 -init_pps ();
    5.19 +
    5.20  print_depth 8;
    5.21  
    5.22  val FOLP_build_completed = ();  (*indicate successful build*)
     6.1 --- a/src/HOL/Auth/DB-ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
     6.2 +++ b/src/HOL/Auth/DB-ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
     6.3 @@ -12,7 +12,4 @@
     6.4  val banner = "Security Protocols";
     6.5  writeln banner;
     6.6  
     6.7 -init_thy_reader();
     6.8 -
     6.9  use_thy "Message";
    6.10 -
     7.1 --- a/src/HOL/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
     7.2 +++ b/src/HOL/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
     7.3 @@ -49,7 +49,6 @@
     7.4  use "sys.sml";
     7.5  cd "../HOL";
     7.6  
     7.7 -init_pps ();
     7.8  print_depth 8;
     7.9  
    7.10  val HOL_build_completed = ();   (*indicate successful build*)
     8.1 --- a/src/HOL/thy_data.ML	Wed Jul 09 16:54:17 1997 +0200
     8.2 +++ b/src/HOL/thy_data.ML	Wed Jul 09 17:00:34 1997 +0200
     8.3 @@ -106,7 +106,7 @@
     8.4  end;
     8.5  
     8.6  (*Must be redefined in order to refer to the new instance of bind_thm
     8.7 -  created by init_thy_reader.*)
     8.8 +  created by init_thy_reader.*)		(* FIXME: move *)
     8.9  
    8.10  fun qed_spec_mp name =
    8.11    let val thm = normalize_thm [RSspec,RSmp] (result())
     9.1 --- a/src/HOLCF/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
     9.2 +++ b/src/HOLCF/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
     9.3 @@ -32,7 +32,6 @@
     9.4  use "domain/interface.ML";
     9.5  
     9.6  init_thy_reader();
     9.7 -init_pps ();
     9.8  
     9.9  fun qed_spec_mp name =
    9.10    let val thm = normalize_thm [RSspec,RSmp] (result())
    10.1 --- a/src/Sequents/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
    10.2 +++ b/src/Sequents/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
    10.3 @@ -9,8 +9,6 @@
    10.4  val banner = "Sequent Calculii";
    10.5  writeln banner;
    10.6  
    10.7 -init_thy_reader();
    10.8 -
    10.9  print_depth 1;  
   10.10  
   10.11  use_thy "Sequents";
   10.12 @@ -24,7 +22,6 @@
   10.13  use_thy"S4";
   10.14  use_thy"S43";
   10.15  
   10.16 -init_pps ();
   10.17  print_depth 8;
   10.18  
   10.19  val Sequents_build_completed = ();    (*indicate successful build*)