src/CTT/ROOT.ML
changeset 3929 3553fcfa2c7e
parent 3511 da4dd8b7ced4
child 4222 d7573d6d0513
equal deleted inserted replaced
3928:787d2659ce4a 3929:3553fcfa2c7e
     8 *)
     8 *)
     9 
     9 
    10 val banner = "Constructive Type Theory";
    10 val banner = "Constructive Type Theory";
    11 writeln banner;
    11 writeln banner;
    12 
    12 
       
    13 reset global_names;
       
    14 
    13 print_depth 1;  
    15 print_depth 1;  
    14 
    16 
    15 use_thy "CTT";
    17 use_thy "CTT";
    16 use "../Provers/typedsimp.ML";
    18 use "../Provers/typedsimp.ML";
    17 use "rew.ML";
    19 use "rew.ML";