223 |
223 |
224 fun lemma_tac th i = |
224 fun lemma_tac th i = |
225 rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i; |
225 rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i; |
226 *} |
226 *} |
227 |
227 |
228 method_setup fast_prop = |
228 method_setup fast_prop = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *} |
229 {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *} |
229 method_setup fast = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *} |
230 "propositional reasoning" |
230 method_setup fast_dup = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *} |
231 |
231 method_setup best = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *} |
232 method_setup fast = |
232 method_setup best_dup = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *} |
233 {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *} |
|
234 "classical reasoning" |
|
235 |
|
236 method_setup fast_dup = |
|
237 {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *} |
|
238 "classical reasoning" |
|
239 |
|
240 method_setup best = |
|
241 {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *} |
|
242 "classical reasoning" |
|
243 |
|
244 method_setup best_dup = |
|
245 {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *} |
|
246 "classical reasoning" |
|
247 |
233 |
248 |
234 |
249 lemma mp_R: |
235 lemma mp_R: |
250 assumes major: "$H |- $E, $F, P --> Q" |
236 assumes major: "$H |- $E, $F, P --> Q" |
251 and minor: "$H |- $E, $F, P" |
237 and minor: "$H |- $E, $F, P" |