src/Pure/drule.ML
changeset 11960 58ffa8bec4da
parent 11815 ef7619398680
child 11975 129c6679e8c4
     1.1 --- a/src/Pure/drule.ML	Sat Oct 27 00:06:22 2001 +0200
     1.2 +++ b/src/Pure/drule.ML	Sat Oct 27 00:06:46 2001 +0200
     1.3 @@ -97,6 +97,7 @@
     1.4    val internalK         : string
     1.5    val kind_internal     : 'a attribute
     1.6    val has_internal      : tag list -> bool
     1.7 +  val impose_hyps       : cterm list -> thm -> thm
     1.8    val close_derivation  : thm -> thm
     1.9    val compose_single    : thm * int * thm -> thm
    1.10    val add_rules         : thm list -> thm list -> thm list
    1.11 @@ -318,6 +319,10 @@
    1.12  (* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
    1.13  fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths);
    1.14  
    1.15 +(* maps |- B to A1,...,An |- B *)
    1.16 +fun impose_hyps chyps th =
    1.17 +  implies_elim_list (implies_intr_list chyps th) (map Thm.assume chyps);
    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;