src/LCF/ROOT.ML
changeset 121 d392174734e9
parent 72 099d949fe467
child 1296 ae31bb7774a7
equal deleted inserted replaced
120:09287f26bfb8 121:d392174734e9
     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 
       
    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";
    21 
    19 
    22 val LCF_build_completed = ();	(*indicate successful build*)
    20 val LCF_build_completed = ();	(*indicate successful build*)