src/HOL/Orderings.thy
changeset 30722 623d4831c8cf
parent 30528 7173bf123335
child 30806 342c73345237
     1.1 --- a/src/HOL/Orderings.thy	Wed Mar 25 21:35:49 2009 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Thu Mar 26 14:14:02 2009 +0100
     1.3 @@ -372,13 +372,14 @@
     1.4    Thm.declaration_attribute
     1.5      (fn _ => Data.map (AList.delete struct_eq s));
     1.6  
     1.7 -val attribute =
     1.8 -  Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
     1.9 -      Args.del >> K NONE) --| Args.colon (* FIXME ||
    1.10 -    Scan.succeed true *) ) -- Scan.lift Args.name --
    1.11 -  Scan.repeat Args.term
    1.12 -  >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
    1.13 -       | ((NONE, n), ts) => del_struct (n, ts));
    1.14 +val attrib_setup =
    1.15 +  Attrib.setup @{binding order}
    1.16 +    (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
    1.17 +      Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
    1.18 +      Scan.repeat Args.term
    1.19 +      >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
    1.20 +           | ((NONE, n), ts) => del_struct (n, ts)))
    1.21 +    "theorems controlling transitivity reasoner";
    1.22  
    1.23  
    1.24  (** Diagnostic command **)
    1.25 @@ -397,8 +398,9 @@
    1.26  (** Setup **)
    1.27  
    1.28  val setup =
    1.29 -  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
    1.30 -  Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
    1.31 +  Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac []))
    1.32 +    "transitivity reasoner" #>
    1.33 +  attrib_setup;
    1.34  
    1.35  end;
    1.36