--- a/src/Sequents/ILL.thy Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Sequents/ILL.thy Fri Mar 13 19:58:26 2009 +0100
@@ -146,7 +146,7 @@
*}
method_setup best_lazy =
- {* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *}
+ {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
"lazy classical reasoning"
lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
@@ -282,10 +282,10 @@
method_setup best_safe =
- {* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} ""
+ {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
method_setup best_power =
- {* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} ""
+ {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
(* Some examples from Troelstra and van Dalen *)