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 (Method.SIMPLE_METHOD' HEADGOAL (best_tac lazy_cs)) *} |
149 {* Method.no_args (Method.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) |
155 apply (rule_tac [2] identity) |
155 apply (rule_tac [2] identity) |
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 (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} "" |
285 {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} "" |
286 |
286 |
287 method_setup best_power = |
287 method_setup best_power = |
288 {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} "" |
288 {* Method.no_args (Method.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" |