src/LCF/ROOT.ML
changeset 4905 be73ddff6c5a
parent 4024 3c056eab237c
child 6349 f7750d816c21
equal deleted inserted replaced
4904:5f6b2dd1cd11 4905:be73ddff6c5a
    12 writeln banner;
    12 writeln banner;
    13 
    13 
    14 print_depth 1;
    14 print_depth 1;
    15 use_thy "LCF";
    15 use_thy "LCF";
    16 use"simpdata.ML";
    16 use"simpdata.ML";
    17 use"pair.ML";
    17 use_thy"pair";
    18 use"fix.ML";
    18 use_thy"fix";
    19 
    19 
    20 val LCF_build_completed = ();   (*indicate successful build*)
    20 val LCF_build_completed = ();   (*indicate successful build*)