load simplifier.ML (again);
authorwenzelm
Fri Jul 25 13:18:45 1997 +0200 (1997-07-25)
changeset 3578b2b9a9ddb9cc
parent 3577 9715b6e3ec5f
child 3579 8bd9b4b3b61d
load simplifier.ML (again);
src/FOL/ROOT.ML
src/HOL/ROOT.ML
     1.1 --- a/src/FOL/ROOT.ML	Fri Jul 25 13:18:09 1997 +0200
     1.2 +++ b/src/FOL/ROOT.ML	Fri Jul 25 13:18:45 1997 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4  
     1.5  print_depth 1;  
     1.6  
     1.7 +use "../Provers/simplifier.ML";
     1.8  use "../Provers/splitter.ML";
     1.9  use "../Provers/ind.ML";
    1.10  use "../Provers/hypsubst.ML";
     2.1 --- a/src/HOL/ROOT.ML	Fri Jul 25 13:18:09 1997 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Fri Jul 25 13:18:45 1997 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4  use "../Pure/section_utils.ML";
     2.5  use "thy_syntax.ML";
     2.6  
     2.7 +use "../Provers/simplifier.ML";
     2.8  use "../Provers/splitter.ML";
     2.9  use "../Provers/hypsubst.ML";
    2.10  use "../Provers/classical.ML";