src/LCF/ROOT.ML
changeset 4024 3c056eab237c
parent 3941 ea440c63d206
child 4905 be73ddff6c5a
equal deleted inserted replaced
4023:a9dc0484c903 4024:3c056eab237c
     9 *)
     9 *)
    10 
    10 
    11 val banner = "Logic for Computable Functions (in FOL)";
    11 val banner = "Logic for Computable Functions (in FOL)";
    12 writeln banner;
    12 writeln banner;
    13 
    13 
    14 reset global_names;
       
    15 
       
    16 print_depth 1;
    14 print_depth 1;
    17 use_thy "LCF";
    15 use_thy "LCF";
    18 use"simpdata.ML";
    16 use"simpdata.ML";
    19 use"pair.ML";
    17 use"pair.ML";
    20 use"fix.ML";
    18 use"fix.ML";