src/HOL/Transitive_Closure.thy
changeset 30510 4120fc59dd85
parent 30242 aea5d7fa7ef5
child 30549 d2d7874648bd
--- a/src/HOL/Transitive_Closure.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -695,16 +695,16 @@
 (* Optional methods *)
 
 method_setup trancl =
-  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
   {* simple transitivity reasoner *}
 method_setup rtrancl =
-  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
   {* simple transitivity reasoner *}
 method_setup tranclp =
-  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
   {* simple transitivity reasoner (predicate version) *}
 method_setup rtranclp =
-  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
+  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
   {* simple transitivity reasoner (predicate version) *}
 
 end