--- a/src/Sequents/LK0.thy Wed Nov 29 15:44:46 2006 +0100
+++ b/src/Sequents/LK0.thy Wed Nov 29 15:44:51 2006 +0100
@@ -248,23 +248,23 @@
*}
method_setup fast_prop =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac prop_pack)) *}
+ {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *}
"propositional reasoning"
method_setup fast =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_pack)) *}
+ {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *}
"classical reasoning"
method_setup fast_dup =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (fast_tac LK_dup_pack)) *}
+ {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
"classical reasoning"
method_setup best =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_pack)) *}
+ {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *}
"classical reasoning"
method_setup best_dup =
- {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (best_tac LK_dup_pack)) *}
+ {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
"classical reasoning"