src/HOL/Transitive_Closure.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 30954 cf50e67bc1d1
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -695,16 +695,16 @@
     1.4  (* Optional methods *)
     1.5  
     1.6  method_setup trancl =
     1.7 -  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
     1.8 +  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
     1.9    {* simple transitivity reasoner *}
    1.10  method_setup rtrancl =
    1.11 -  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
    1.12 +  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
    1.13    {* simple transitivity reasoner *}
    1.14  method_setup tranclp =
    1.15 -  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
    1.16 +  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
    1.17    {* simple transitivity reasoner (predicate version) *}
    1.18  method_setup rtranclp =
    1.19 -  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
    1.20 +  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
    1.21    {* simple transitivity reasoner (predicate version) *}
    1.22  
    1.23  end