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