src/HOL/Orderings.thy
changeset 24867 e5b55d7be9bb
parent 24748 ee0a0eb6b738
child 24920 2a45e400fdad
     1.1 --- a/src/HOL/Orderings.thy	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -346,7 +346,7 @@
     1.4      (Context.cases (print_structures o ProofContext.init) print_structures)
     1.5      (print_structures o Proof.context_of));
     1.6  
     1.7 -val printP =
     1.8 +val _ =
     1.9    OuterSyntax.improper_command "print_orders"
    1.10      "print order structures available to transitivity reasoner" OuterKeyword.diag
    1.11      (Scan.succeed (Toplevel.no_timing o print));
    1.12 @@ -354,11 +354,10 @@
    1.13  
    1.14  (** Setup **)
    1.15  
    1.16 -val setup = let val _ = OuterSyntax.add_parsers [printP] in
    1.17 -    Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []),
    1.18 -      "normalisation of algebraic structure")] #>
    1.19 -    Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]
    1.20 -  end;
    1.21 +val setup =
    1.22 +  Method.add_methods
    1.23 +    [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #>
    1.24 +  Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
    1.25  
    1.26  end;
    1.27