--- a/src/Pure/drule.ML Sat Oct 27 00:06:22 2001 +0200
+++ b/src/Pure/drule.ML Sat Oct 27 00:06:46 2001 +0200
@@ -97,6 +97,7 @@
val internalK : string
val kind_internal : 'a attribute
val has_internal : tag list -> bool
+ val impose_hyps : cterm list -> thm -> thm
val close_derivation : thm -> thm
val compose_single : thm * int * thm -> thm
val add_rules : thm list -> thm list -> thm list
@@ -318,6 +319,10 @@
(* maps [| A1;...;An |] ==> B and [A1,...,An] to B *)
fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
+(* maps |- B to A1,...,An |- B *)
+fun impose_hyps chyps th =
+ implies_elim_list (implies_intr_list chyps th) (map Thm.assume chyps);
+
(*Reset Var indexes to zero, renaming to preserve distinctness*)
fun zero_var_indexes th =
let val {prop,sign,...} = rep_thm th;