src/Cube/ROOT.ML
changeset 72 099d949fe467
parent 0 a5a9c433f639
child 121 d392174734e9
equal deleted inserted replaced
71:729fe026c5f3 72:099d949fe467
     7 *)
     7 *)
     8 
     8 
     9 val banner = "Barendregt's Lambda-Cube";
     9 val banner = "Barendregt's Lambda-Cube";
    10 writeln banner;
    10 writeln banner;
    11 
    11 
       
    12 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
       
    13 open Readthy;
       
    14 
    12 print_depth 1;  
    15 print_depth 1;  
    13 use_thy "cube";
    16 use_thy "cube";
    14 
    17 
    15 use "../Pure/install_pp.ML";
    18 use "../Pure/install_pp.ML";
    16 print_depth 8;
    19 print_depth 8;