src/Pure/tactic.ML

   val rewrite_goals_tac: thm list -> tactic
   val rewrite_tac: thm list -> tactic
   val rewtac: thm -> tactic
   val rtac: thm -> int -> tactic
   val rule_by_tactic: tactic -> thm -> thm
+  val subgoal_tac: string -> int -> tactic
+  val subgoals_tac: string list -> int -> tactic
   val subgoals_of_brl: bool * thm -> int
-  val subgoal_tac: string -> int -> tactic
   val trace_goalno_tac: (int -> tactic) -> int -> tactic
   end
 end;
 
 

     EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
 
 (*Introduce the given proposition as a lemma and subgoal*)
 fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl;
 
+(*Introduce a list of lemmas and subgoals*)
+fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
+
 
 (**** Indexing and filtering of theorems ****)
 
 (*Returns the list of potentially resolvable theorems for the goal "prem",
 	using the predicate  could(subgoal,concl).