src/HOL/Orderings.thy

 
 signature ORDERS =
 sig
   val print_structures: Proof.context -> unit
   val setup: theory -> theory
-  val order_tac: Proof.context -> int -> tactic
+  val order_tac: thm list -> Proof.context -> int -> tactic
 end;
 
 structure Orders: ORDERS =
 struct
 

   end;
 
 
 (** Method **)
 
-fun struct_tac ((s, [eq, le, less]), thms) =
+fun struct_tac ((s, [eq, le, less]), thms) prems =
   let
     fun decomp thy (Trueprop $ t) =
       let
         fun excluded t =
           (* exclude numeric types: linear arithmetic subsumes transitivity *)

               else NONE
 	  | dec _ = NONE;
       in dec t end;
   in
     case s of
-      "order" => Order_Tac.partial_tac decomp thms
-    | "linorder" => Order_Tac.linear_tac decomp thms
+      "order" => Order_Tac.partial_tac decomp thms prems
+    | "linorder" => Order_Tac.linear_tac decomp thms prems
     | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
   end
 
-fun order_tac ctxt =
-  FIRST' (map (fn s => CHANGED o struct_tac s) (Data.get (Context.Proof ctxt)));
+fun order_tac prems ctxt =
+  FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt)));
 
 
 (** Attribute **)
 
 fun add_struct_thm s tag =

 
 
 (** Setup **)
 
 val setup = let val _ = OuterSyntax.add_parsers [printP] in
-    Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac),
+    Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []),
       "normalisation of algebraic structure")] #>
     Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]
   end;
 
 end;

   (Simplifier.change_simpset_of thy (fn ss => ss
     addsimprocs (map (fn (name, raw_ts, proc) =>
       Simplifier.simproc thy name raw_ts proc)) procs); thy);
 fun add_solver name tac thy =
   (Simplifier.change_simpset_of thy (fn ss => ss addSolver
-    (mk_solver' name (fn ss => tac (MetaSimplifier.the_context ss)))); thy);
+    (mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy);
 
 in
   add_simprocs [
        ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
        ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)