equal
deleted
inserted
replaced
58 |
58 |
59 (EX x y z. ...) | ... | (EX a b c. ...) |
59 (EX x y z. ...) | ... | (EX a b c. ...) |
60 *) |
60 *) |
61 fun atomize_elim_conv ctxt ct = |
61 fun atomize_elim_conv ctxt ct = |
62 (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt |
62 (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt |
63 then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt) |
63 then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt) |
64 then_conv (fn ct' => if can Object_Logic.dest_judgment ct' |
64 then_conv (fn ct' => if can Object_Logic.dest_judgment ct' |
65 then all_conv ct' |
65 then all_conv ct' |
66 else raise CTERM ("atomize_elim", [ct', ct]))) |
66 else raise CTERM ("atomize_elim", [ct', ct]))) |
67 ct |
67 ct |
68 |
68 |