equal
deleted
inserted
replaced
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*) |