src/CTT/ROOT.ML
changeset 393 02b27671b899
parent 121 d392174734e9
child 1294 1358dc040edb
equal deleted inserted replaced
392:674d878719bd 393:02b27671b899
    10 val banner = "Constructive Type Theory";
    10 val banner = "Constructive Type Theory";
    11 writeln banner;
    11 writeln banner;
    12 
    12 
    13 print_depth 1;  
    13 print_depth 1;  
    14 
    14 
    15 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
    15 init_thy_reader();
    16 open Readthy;
       
    17 
    16 
    18 use_thy "CTT";
    17 use_thy "CTT";
    19 use "../Provers/typedsimp.ML";
    18 use "../Provers/typedsimp.ML";
    20 use "rew.ML";
    19 use "rew.ML";
    21 use_thy "Arith";
    20 use_thy "Arith";