equal
deleted
inserted
replaced
192 ORELSE' eresolve_tac ctxt elims |
192 ORELSE' eresolve_tac ctxt elims |
193 ORELSE' (eresolve_tac ctxt [@{thm impE1}] THEN' assume_tac ctxt) |
193 ORELSE' (eresolve_tac ctxt [@{thm impE1}] THEN' assume_tac ctxt) |
194 end\<close> |
194 end\<close> |
195 |
195 |
196 text \<open> |
196 text \<open> |
197 In Line 11 we apply the rule @{thm [source] impE1} in concjunction |
197 In Line 9 we apply the rule @{thm [source] impE1} in concjunction |
198 with @{ML assume_tac} in order to reduce the number of possibilities that |
198 with @{ML assume_tac} in order to reduce the number of possibilities that |
199 need to be explored. You can use the tactic as follows. |
199 need to be explored. You can use the tactic as follows. |
200 \<close> |
200 \<close> |
201 |
201 |
202 lemma |
202 lemma |