--- a/src/Sequents/ILL.thy Wed Nov 29 15:44:46 2006 +0100
+++ b/src/Sequents/ILL.thy Wed Nov 29 15:44:51 2006 +0100
@@ -146,8 +146,8 @@
*}
method_setup best_lazy =
-{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac lazy_cs)) *}
-"lazy classical reasoning"
+ {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *}
+ "lazy classical reasoning"
lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
apply (rule derelict)
@@ -282,10 +282,10 @@
method_setup best_safe =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac safe_cs)) *} ""
+ {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} ""
method_setup best_power =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac power_cs)) *} ""
+ {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} ""
(* Some examples from Troelstra and van Dalen *)