src/LCF/ROOT.ML
changeset 72 099d949fe467
parent 0 a5a9c433f639
child 121 d392174734e9
equal deleted inserted replaced
71:729fe026c5f3 72:099d949fe467
     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 set_loadpath [".", "../FOL"];
       
    15 
    14 print_depth 1;
    16 print_depth 1;
    15 use_thy "lcf";
    17 use_thy "lcf";
    16 use"simpdata.ML";
    18 use"simpdata.ML";
    17 use"pair.ML";
    19 use"pair.ML";
    18 use"fix.ML";
    20 use"fix.ML";