--- 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 ****)