src/Pure/simplifier.ML

   include BASIC_SIMPLIFIER
   val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
   val attrib: (thm -> Proof.context -> Proof.context) -> attribute
   val simp_add: attribute
   val simp_del: attribute
+  val simp_reorient: attribute
   val cong_add: attribute
   val cong_del: attribute
   val check_simproc: Proof.context -> xstring * Position.T -> string
   val the_simproc: Proof.context -> string -> simproc
   type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}

 
 fun attrib f = Thm.declaration_attribute (map_ss o f);
 
 val simp_add = attrib add_simp;
 val simp_del = attrib del_simp;
+val simp_reorient = attrib reorient_simp;
 val cong_add = attrib add_cong;
 val cong_del = attrib del_cong;
 
 
 (** named simprocs **)

 (** concrete syntax of attributes **)
 
 (* add / del *)
 
 val simpN = "simp";
+val reorientN = "reorient"
 val congN = "cong";
 val onlyN = "only";
 val no_asmN = "no_asm";
 val no_asm_useN = "no_asm_use";
 val no_asm_simpN = "no_asm_simp";

 
 val simp_modifiers =
  [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
+  Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
    @ cong_modifiers;
 
 val simp_modifiers' =
  [Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
+  Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
   Args.$$$ onlyN -- Args.colon >>
     K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
    @ cong_modifiers;
 
 val simp_options =