src/Cube/ROOT.ML
changeset 4024 3c056eab237c
parent 3941 ea440c63d206
child 6349 f7750d816c21
equal deleted inserted replaced
4023:a9dc0484c903 4024:3c056eab237c
     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 reset global_names;
       
    13 
       
    14 print_depth 1;  
    12 print_depth 1;  
    15 
    13 
    16 use_thy "Cube";
    14 use_thy "Cube";
    17 
    15 
    18 print_depth 8;
    16 print_depth 8;