--- a/src/Pure/tactic.ML Mon Nov 09 15:40:05 1998 +0100
+++ b/src/Pure/tactic.ML Mon Nov 09 15:40:26 1998 +0100
@@ -60,7 +60,8 @@
val make_elim : thm -> thm
val match_from_net_tac : (int*thm) Net.net -> int -> tactic
val match_tac : thm list -> int -> tactic
- val metacut_tac : thm -> int -> tactic
+ val metacut_tac : thm -> int -> tactic
+ val metacuts_tac : thm list -> int -> tactic
val net_bimatch_tac : (bool*thm) list -> int -> tactic
val net_biresolve_tac : (bool*thm) list -> int -> tactic
val net_match_tac : thm list -> int -> tactic
@@ -321,6 +322,7 @@
(*The conclusion of the rule gets assumed in subgoal i,
while subgoal i+1,... are the premises of the rule.*)
fun metacut_tac rule = bires_cut_tac [(false,rule)];
+fun metacuts_tac rules i = EVERY (map (fn th => metacut_tac th i) rules);
(*Recognizes theorems that are not rules, but simple propositions*)
fun is_fact rl =