src/FOLP/ROOT.ML
changeset 3942 1f1c1f524d19
parent 3836 f1a1817659e6
child 4024 3c056eab237c
equal deleted inserted replaced
3941:ea440c63d206 3942:1f1c1f524d19
     9 *)
     9 *)
    10 
    10 
    11 val banner = "First-Order Logic with Natural Deduction with Proof Terms";
    11 val banner = "First-Order Logic with Natural Deduction with Proof Terms";
    12 
    12 
    13 writeln banner;
    13 writeln banner;
       
    14 
       
    15 reset global_names;
    14 
    16 
    15 print_depth 1;
    17 print_depth 1;
    16 
    18 
    17 use_thy "IFOLP";
    19 use_thy "IFOLP";
    18 use_thy "FOLP";
    20 use_thy "FOLP";