# HG changeset patch
# User lcp
# Date 772447502 -7200
# Node ID ad3f46c13f1e0682afdc51bcc5be18bbdad2306e
# Parent  52e8393ccd7750fa3deb6edb9fbf4c102ba0e4d0
Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)

diff -r 52e8393ccd77 -r ad3f46c13f1e src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Jun 23 17:52:58 1994 +0200
+++ b/src/Pure/tactic.ML	Fri Jun 24 10:45:02 1994 +0200
@@ -66,8 +66,9 @@
   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;
@@ -261,6 +262,9 @@
 (*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 ****)