equal
deleted
inserted
replaced
144 |
144 |
145 end |
145 end |
146 *} |
146 *} |
147 |
147 |
148 method_setup best_lazy = |
148 method_setup best_lazy = |
149 {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *} |
149 {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *} |
150 "lazy classical reasoning" |
150 "lazy classical reasoning" |
151 |
151 |
152 lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B" |
152 lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B" |
153 apply (rule derelict) |
153 apply (rule derelict) |
154 apply (rule impl) |
154 apply (rule impl) |
280 val power_cs = safe_cs add_unsafes [thm "impr_contr_der"]; |
280 val power_cs = safe_cs add_unsafes [thm "impr_contr_der"]; |
281 *} |
281 *} |
282 |
282 |
283 |
283 |
284 method_setup best_safe = |
284 method_setup best_safe = |
285 {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} "" |
285 {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} "" |
286 |
286 |
287 method_setup best_power = |
287 method_setup best_power = |
288 {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} "" |
288 {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} "" |
289 |
289 |
290 |
290 |
291 (* Some examples from Troelstra and van Dalen *) |
291 (* Some examples from Troelstra and van Dalen *) |
292 |
292 |
293 lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0" |
293 lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0" |