src/HOLCF/FOCUS/ROOT.ML
changeset 16844 60ab395e6da5
parent 15188 9d57263faf9e
child 24106 f2965bf954dc
equal deleted inserted replaced
16843:8ff9a80f3c93 16844:60ab395e6da5
     7 *)
     7 *)
     8 
     8 
     9 val banner = "HOLCF/FOCUS";
     9 val banner = "HOLCF/FOCUS";
    10 writeln banner;
    10 writeln banner;
    11 
    11 
    12 use_thy "Fstreams";
    12 with_path "~~/src/HOLCF/ex" use_thy "Fstreams";
    13 use_thy "FOCUS";
    13 use_thy "FOCUS";
    14 use_thy "Buffer_adm";
    14 use_thy "Buffer_adm";