# HG changeset patch
# User wenzelm
# Date 910622426 -3600
# Node ID a4122945d638efdc21c7c174a7ceb30b173e0273
# Parent  ce9a8b05d652904a4ae2ed6ff880184ed31bfb2f
added metacuts_tac;

diff -r ce9a8b05d652 -r a4122945d638 src/Pure/tactic.ML
--- 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 =