src/HOLCF/ROOT.ML
changeset 3953 473ea5ce5ca8
parent 3623 e843c1d6f9e1
child 4008 2444085532c6
equal deleted inserted replaced
3952:dca1bce88ec8 3953:473ea5ce5ca8
     7 Should be executed in subdirectory HOLCF.
     7 Should be executed in subdirectory HOLCF.
     8 *)
     8 *)
     9 
     9 
    10 val banner = "HOLCF";
    10 val banner = "HOLCF";
    11 writeln banner;
    11 writeln banner;
       
    12 
       
    13 set global_names;
    12 
    14 
    13 print_depth 1;
    15 print_depth 1;
    14 
    16 
    15 use_thy "HOLCF";
    17 use_thy "HOLCF";
    16 
    18