# HG changeset patch
# User wenzelm
# Date 1003266021 -7200
# Node ID ef76193986806aa4749029ce6f98f2daf136f753
# Parent  1de4a3321976db8c25514972479cc61d083ddd22
added implies_intr_goals;

diff -r 1de4a3321976 -r ef7619398680 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Oct 16 22:59:30 2001 +0200
+++ b/src/Pure/drule.ML	Tue Oct 16 23:00:21 2001 +0200
@@ -96,26 +96,25 @@
   val corollaryK        : string
   val internalK         : string
   val kind_internal     : 'a attribute
-  val has_internal	: tag list -> bool
+  val has_internal      : tag list -> bool
   val close_derivation  : thm -> thm
   val compose_single    : thm * int * thm -> thm
-  val add_rules		: thm list -> thm list -> thm list
-  val del_rules		: thm list -> thm list -> thm list
-  val merge_rules	: thm list * thm list -> thm list
-  val norm_hhf_eq	: thm
+  val add_rules         : thm list -> thm list -> thm list
+  val del_rules         : thm list -> thm list -> thm list
+  val merge_rules       : thm list * thm list -> thm list
+  val norm_hhf_eq       : thm
   val triv_goal         : thm
   val rev_triv_goal     : thm
+  val implies_intr_goals: cterm list -> thm -> thm
   val freeze_all        : thm -> thm
   val mk_triv_goal      : cterm -> thm
-  val mk_cgoal          : cterm -> cterm
-  val assume_goal       : cterm -> thm
   val tvars_of_terms    : term list -> (indexname * sort) list
   val vars_of_terms     : term list -> (indexname * typ) list
   val tvars_of          : thm -> (indexname * sort) list
   val vars_of           : thm -> (indexname * typ) list
   val unvarifyT         : thm -> thm
   val unvarify          : thm -> thm
-  val tvars_intr_list	: string list -> thm -> thm
+  val tvars_intr_list   : string list -> thm -> thm
 end;
 
 structure Drule: DRULE =
@@ -313,7 +312,7 @@
 (*Specialization over a list of cterms*)
 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th);
 
-(* maps [A1,...,An], B   to   [| A1;...;An |] ==> B  *)
+(* maps A1,...,An |- B   to   [| A1;...;An |] ==> B  *)
 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th);
 
 (* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
@@ -392,7 +391,7 @@
    Any remaining trailing positions are left unchanged. *)
 val rearrange_prems = let
   fun rearr new []      thm = thm
-  |   rearr new (p::ps) thm = rearr (new+1) 
+  |   rearr new (p::ps) thm = rearr (new+1)
      (map (fn q => if new<=q andalso q<p then q+1 else q) ps)
      (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
   in rearr 0 end;
@@ -752,6 +751,10 @@
 val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const);
 fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal;
 
+fun implies_intr_goals cprops thm =
+  implies_elim_list (implies_intr_list cprops thm) (map assume_goal cprops)
+  |> implies_intr_list (map mk_cgoal cprops);
+
 
 
 (** variations on instantiate **)