src/HOL/Transitive_Closure.thy
changeset 30510 4120fc59dd85
parent 30242 aea5d7fa7ef5
child 30549 d2d7874648bd
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -695,16 +695,16 @@
     1.4  (* Optional methods *)
     1.5  
     1.6  method_setup trancl =
     1.7 -  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
     1.8 +  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
     1.9    {* simple transitivity reasoner *}
    1.10  method_setup rtrancl =
    1.11 -  {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
    1.12 +  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
    1.13    {* simple transitivity reasoner *}
    1.14  method_setup tranclp =
    1.15 -  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
    1.16 +  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
    1.17    {* simple transitivity reasoner (predicate version) *}
    1.18  method_setup rtranclp =
    1.19 -  {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
    1.20 +  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
    1.21    {* simple transitivity reasoner (predicate version) *}
    1.22  
    1.23  end