added satisfy_hyps;
authorwenzelm
Thu Jul 18 12:05:51 2002 +0200 (2002-07-18)
changeset 133890cbda884a7e5
parent 13388 eff0ede61da1
child 13390 c48c634605f1
added satisfy_hyps;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Thu Jul 18 12:05:29 2002 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Jul 18 12:05:51 2002 +0200
     1.3 @@ -101,6 +101,7 @@
     1.4    val kind_internal: 'a attribute
     1.5    val has_internal: tag list -> bool
     1.6    val impose_hyps: cterm list -> thm -> thm
     1.7 +  val satisfy_hyps: thm list -> thm -> thm
     1.8    val close_derivation: thm -> thm
     1.9    val local_standard: thm -> thm
    1.10    val compose_single: thm * int * thm -> thm
    1.11 @@ -350,6 +351,10 @@
    1.12    let val chyps' = gen_rems (op aconv o apfst Thm.term_of) (chyps, #hyps (Thm.rep_thm th))
    1.13    in implies_elim_list (implies_intr_list chyps' th) (map Thm.assume chyps') end;
    1.14  
    1.15 +(* maps A1,...,An and A1,...,An |- B to |- B *)
    1.16 +fun satisfy_hyps ths th =
    1.17 +  implies_elim_list (implies_intr_list (map (#prop o Thm.crep_thm) ths) th) ths;
    1.18 +
    1.19  (*Reset Var indexes to zero, renaming to preserve distinctness*)
    1.20  fun zero_var_indexes th =
    1.21      let val {prop,sign,...} = rep_thm th;