src/Cube/ROOT.ML
changeset 393 02b27671b899
parent 121 d392174734e9
child 1296 ae31bb7774a7
equal deleted inserted replaced
392:674d878719bd 393:02b27671b899
     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);
    12 init_thy_reader();
    13 open Readthy;
       
    14 
    13 
    15 print_depth 1;  
    14 print_depth 1;  
    16 use_thy "Cube";
    15 use_thy "Cube";
    17 
    16 
    18 use "../Pure/install_pp.ML";
    17 use "../Pure/install_pp.ML";