src/CTT/ROOT.ML
changeset 17441 5b5feca0344a
parent 10466 78168ca70469
child 19761 5cd82054c2c6
equal deleted inserted replaced
17440:df77edc4f5d0 17441:5b5feca0344a
     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 print_depth 1;  
       
    14 
       
    15 use_thy "CTT";
       
    16 use "~~/src/Provers/typedsimp.ML";
       
    17 use "rew.ML";
       
    18 use_thy "Main";
    13 use_thy "Main";
    19 
    14 
    20 print_depth 8;
       
    21 
       
    22 Goal "tt : T";  (*leave subgoal package empty*)
    15 Goal "tt : T";  (*leave subgoal package empty*)