src/Sequents/LK0.thy
changeset 30510 4120fc59dd85
parent 27239 f2f42f9fa09d
child 30549 d2d7874648bd
--- a/src/Sequents/LK0.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Sequents/LK0.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -240,23 +240,23 @@
 *}
 
 method_setup fast_prop =
-  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac prop_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *}
   "propositional reasoning"
 
 method_setup fast =
-  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *}
   "classical reasoning"
 
 method_setup fast_dup =
-  {* Method.no_args (Method.SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
   "classical reasoning"
 
 method_setup best =
-  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *}
   "classical reasoning"
 
 method_setup best_dup =
-  {* Method.no_args (Method.SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
+  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
   "classical reasoning"