src/FOL/ROOT.ML
changeset 7576 594f09166c38
parent 7355 4c43090659ca
child 9157 998dd2fb5795
equal deleted inserted replaced
7575:e1e2d07287d8 7576:594f09166c38
    19 use "~~/src/Provers/classical.ML";
    19 use "~~/src/Provers/classical.ML";
    20 use "~~/src/Provers/blast.ML";
    20 use "~~/src/Provers/blast.ML";
    21 use "~~/src/Provers/clasimp.ML";
    21 use "~~/src/Provers/clasimp.ML";
    22 use "~~/src/Provers/quantifier1.ML";
    22 use "~~/src/Provers/quantifier1.ML";
    23 
    23 
    24 use_thy "IFOL";
       
    25 use_thy "FOL";
    24 use_thy "FOL";
    26 
    25 
    27 print_depth 8;
    26 print_depth 8;