src/CTT/ROOT.ML
changeset 3511 da4dd8b7ced4
parent 2237 f01ac387e82b
child 3929 3553fcfa2c7e
equal deleted inserted replaced
3510:24d235feeb2a 3511:da4dd8b7ced4
    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 init_thy_reader();
       
    16 
       
    17 use_thy "CTT";
    15 use_thy "CTT";
    18 use "../Provers/typedsimp.ML";
    16 use "../Provers/typedsimp.ML";
    19 use "rew.ML";
    17 use "rew.ML";
    20 use_thy "Arith";
    18 use_thy "Arith";
    21 use_thy "Bool";
    19 use_thy "Bool";
    22 
    20 
    23 init_pps ();
       
    24 print_depth 8;
    21 print_depth 8;
    25 
    22 
    26 val CTT_build_completed = ();   (*indicate successful build*)
    23 val CTT_build_completed = ();   (*indicate successful build*)