src/CTT/ROOT.ML
changeset 72 099d949fe467
parent 0 a5a9c433f639
child 121 d392174734e9
equal deleted inserted replaced
71:729fe026c5f3 72:099d949fe467
    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);
       
    16 open Readthy;
       
    17 
    15 use_thy"ctt";
    18 use_thy"ctt";
    16 use "../Provers/typedsimp.ML";
    19 use "../Provers/typedsimp.ML";
    17 use "rew.ML";
    20 use "rew.ML";
    18 use_thy "arith";
    21 use_thy "arith";
    19 use_thy "bool";
    22 use_thy "bool";