src/Pure/conv.ML

   val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   val implies_conv: conv -> conv -> conv
   val implies_concl_conv: conv -> conv
   val rewr_conv: thm -> conv
   val rewrs_conv: thm list -> conv
+  val bottom_rewrs_conv: thm list -> Proof.context -> conv
+  val top_rewrs_conv: thm list -> Proof.context -> conv
+  val top_sweep_rewrs_conv: thm list -> Proof.context -> conv
   val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
   val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
   val top_conv: (Proof.context -> conv) -> Proof.context -> conv
   val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
   val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv

   (case Thm.term_of ct of
     Const ("Pure.imp", _) $ _ $ _ => arg_conv cv ct
   | _ => raise CTERM ("implies_concl_conv", [ct]));
 
 
-(* single rewrite step, cf. REWR_CONV in HOL *)
-
+(* rewrite steps *)
+
+(*cf. REWR_CONV in HOL*)
 fun rewr_conv rule ct =
   let
     val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
     val lhs = Thm.lhs_of rule1;
     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;

         in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (Thm.rhs_of rule3)) end;
   in Thm.transitive rule4 (Thm.beta_conversion true (Thm.rhs_of rule4)) end;
 
 fun rewrs_conv rules = first_conv (map rewr_conv rules);
 
+fun bottom_rewrs_conv rewrs = bottom_conv (K (try_conv (rewrs_conv rewrs)));
+fun top_rewrs_conv rewrs = top_conv (K (try_conv (rewrs_conv rewrs)));
+fun top_sweep_rewrs_conv rewrs = top_sweep_conv (K (rewrs_conv rewrs));
+
 
 (* conversions on HHF rules *)
 
 (*rewrite B in \<And>x1 ... xn. B*)
 fun params_conv n cv ctxt ct =