--- a/src/Pure/drule.ML Thu Jul 18 12:05:29 2002 +0200
+++ b/src/Pure/drule.ML Thu Jul 18 12:05:51 2002 +0200
@@ -101,6 +101,7 @@
val kind_internal: 'a attribute
val has_internal: tag list -> bool
val impose_hyps: cterm list -> thm -> thm
+ val satisfy_hyps: thm list -> thm -> thm
val close_derivation: thm -> thm
val local_standard: thm -> thm
val compose_single: thm * int * thm -> thm
@@ -350,6 +351,10 @@
let val chyps' = gen_rems (op aconv o apfst Thm.term_of) (chyps, #hyps (Thm.rep_thm th))
in implies_elim_list (implies_intr_list chyps' th) (map Thm.assume chyps') end;
+(* maps A1,...,An and A1,...,An |- B to |- B *)
+fun satisfy_hyps ths th =
+ implies_elim_list (implies_intr_list (map (#prop o Thm.crep_thm) ths) th) ths;
+
(*Reset Var indexes to zero, renaming to preserve distinctness*)
fun zero_var_indexes th =
let val {prop,sign,...} = rep_thm th;