src/FOLP/ROOT.ML
changeset 2237 f01ac387e82b
parent 1459 d12da312eff4
child 3511 da4dd8b7ced4
equal deleted inserted replaced
2236:c7869a443b14 2237:f01ac387e82b
    73 val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] 
    73 val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] 
    74                           addSEs [exE,ex1E] addEs [all_dupE];
    74                           addSEs [exE,ex1E] addEs [all_dupE];
    75 
    75 
    76 use "simpdata.ML";
    76 use "simpdata.ML";
    77 
    77 
    78 use "../Pure/install_pp.ML";
    78 init_pps ();
    79 print_depth 8;
    79 print_depth 8;
    80 
    80 
    81 val FOLP_build_completed = ();  (*indicate successful build*)
    81 val FOLP_build_completed = ();  (*indicate successful build*)