src/HOL/Orderings.thy
changeset 47432 e1576d13e933
parent 46976 80123a220219
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Orderings.thy	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -312,7 +312,7 @@
     1.4  signature ORDERS =
     1.5  sig
     1.6    val print_structures: Proof.context -> unit
     1.7 -  val setup: theory -> theory
     1.8 +  val attrib_setup: theory -> theory
     1.9    val order_tac: Proof.context -> thm list -> int -> tactic
    1.10  end;
    1.11  
    1.12 @@ -414,19 +414,15 @@
    1.13      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.14          Toplevel.keep (print_structures o Toplevel.context_of)));
    1.15  
    1.16 -
    1.17 -(** Setup **)
    1.18 -
    1.19 -val setup =
    1.20 -  Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt [])))
    1.21 -    "transitivity reasoner" #>
    1.22 -  attrib_setup;
    1.23 -
    1.24  end;
    1.25  
    1.26  *}
    1.27  
    1.28 -setup Orders.setup
    1.29 +setup Orders.attrib_setup
    1.30 +
    1.31 +method_setup order = {*
    1.32 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
    1.33 +*} "transitivity reasoner"
    1.34  
    1.35  
    1.36  text {* Declarations to set up transitivity reasoner of partial and linear orders. *}