src/FOLP/ROOT.ML
changeset 98 329b5ac27f6e
parent 72 099d949fe467
child 176 5729f6757473
     1.1 --- a/src/FOLP/ROOT.ML	Tue Nov 09 13:21:41 1993 +0100
     1.2 +++ b/src/FOLP/ROOT.ML	Tue Nov 09 13:25:07 1993 +0100
     1.3 @@ -16,8 +16,8 @@
     1.4  open Readthy;
     1.5  
     1.6  print_depth 1;  
     1.7 -use_thy "ifolp";
     1.8 -use_thy "folp";
     1.9 +use_thy "IFOLP";
    1.10 +use_thy "FOLP";
    1.11  
    1.12  use "../Provers/hypsubst.ML";
    1.13  use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
    1.14 @@ -47,7 +47,7 @@
    1.15  structure Hypsubst = HypsubstFun(Hypsubst_Data);
    1.16  open Hypsubst;
    1.17  
    1.18 -use "int-prover.ML";
    1.19 +use "intprover.ML";
    1.20  
    1.21  (*** Applying ClassicalFun to create a classical prover ***)
    1.22  structure Classical_Data =