equal
deleted
inserted
replaced
134 predicate variable. Leave other theorems unchanged.*) |
134 predicate variable. Leave other theorems unchanged.*) |
135 fun transform_elim th = |
135 fun transform_elim th = |
136 if is_elimR th then |
136 if is_elimR th then |
137 let val tm = elimR2Fol th |
137 let val tm = elimR2Fol th |
138 val ctm = cterm_of (sign_of_thm th) tm |
138 val ctm = cterm_of (sign_of_thm th) tm |
139 in |
139 in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end |
140 OldGoals.prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th]) |
|
141 end |
|
142 else th; |
140 else th; |
143 |
141 |
144 |
142 |
145 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) |
143 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) |
146 |
144 |