src/HOL/Orderings.thy
changeset 58826 2ed2eaabe3df
parent 57447 87429bdecad5
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Orderings.thy	Wed Oct 29 17:01:44 2014 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Oct 29 19:01:49 2014 +0100
     1.3 @@ -400,6 +400,8 @@
     1.4  sig
     1.5    val print_structures: Proof.context -> unit
     1.6    val order_tac: Proof.context -> thm list -> int -> tactic
     1.7 +  val add_struct: string * term list -> string -> attribute
     1.8 +  val del_struct: string * term list -> attribute
     1.9  end;
    1.10  
    1.11  structure Orders: ORDERS =
    1.12 @@ -483,26 +485,24 @@
    1.13  
    1.14  (* attributes *)
    1.15  
    1.16 -fun add_struct_thm s tag =
    1.17 +fun add_struct s tag =
    1.18    Thm.declaration_attribute
    1.19      (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
    1.20  fun del_struct s =
    1.21    Thm.declaration_attribute
    1.22      (fn _ => Data.map (AList.delete struct_eq s));
    1.23  
    1.24 -val _ =
    1.25 -  Theory.setup
    1.26 -    (Attrib.setup @{binding order}
    1.27 -      (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
    1.28 -        Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
    1.29 -        Scan.repeat Args.term
    1.30 -        >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
    1.31 -             | ((NONE, n), ts) => del_struct (n, ts)))
    1.32 -      "theorems controlling transitivity reasoner");
    1.33 -
    1.34  end;
    1.35  *}
    1.36  
    1.37 +attribute_setup order = {*
    1.38 +  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
    1.39 +    Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
    1.40 +    Scan.repeat Args.term
    1.41 +    >> (fn ((SOME tag, n), ts) => Orders.add_struct (n, ts) tag
    1.42 +         | ((NONE, n), ts) => Orders.del_struct (n, ts))
    1.43 +*} "theorems controlling transitivity reasoner"
    1.44 +
    1.45  method_setup order = {*
    1.46    Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt []))
    1.47  *} "transitivity reasoner"