src/FOL/ROOT.ML
changeset 393 02b27671b899
parent 121 d392174734e9
child 666 4d9f6d83c2bf
equal deleted inserted replaced
392:674d878719bd 393:02b27671b899
     9 
     9 
    10 val banner = "First-Order Logic with Natural Deduction";
    10 val banner = "First-Order Logic with Natural Deduction";
    11 
    11 
    12 writeln banner;
    12 writeln banner;
    13 
    13 
    14 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
    14 init_thy_reader();
    15 open Readthy;
       
    16 
    15 
    17 print_depth 1;  
    16 print_depth 1;  
    18 use_thy "FOL";
    17 use_thy "FOL";
    19 
    18 
    20 use "../Provers/hypsubst.ML";
    19 use "../Provers/hypsubst.ML";