src/HOLCF/ROOT.ML
changeset 4010 59cac65fb751
parent 4008 2444085532c6
child 4041 4df7f385fe9f
equal deleted inserted replaced
4009:6d9bec7b0b9e 4010:59cac65fb751
     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;
       
    14 
    12 
    15 print_depth 1;
    13 print_depth 1;
    16 
    14 
    17 use_thy "HOLCF";
    15 use_thy "HOLCF";
    18 
    16