# HG changeset patch
# User wenzelm
# Date 1003872481 -7200
# Node ID 82139d3dcdd771e497436d4d08a2d961dee419ed
# Parent  df030220a2a86df6ab63eb4afe6216587c3e4f66
added RANGE (from Isar/proof.ML);

diff -r df030220a2a8 -r 82139d3dcdd7 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Tue Oct 23 22:59:14 2001 +0200
+++ b/src/Pure/tctical.ML	Tue Oct 23 23:28:01 2001 +0200
@@ -12,7 +12,7 @@
 
 
 signature TACTICAL =
-  sig
+sig
   type tactic  (* = thm -> thm Seq.seq*)
   val all_tac           : tactic
   val ALLGOALS          : (int -> tactic) -> tactic   
@@ -40,6 +40,7 @@
   val ORELSE'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val pause_tac         : tactic
   val print_tac         : string -> tactic
+  val RANGE             : (int -> tactic) list -> int -> tactic
   val REPEAT            : tactic -> tactic
   val REPEAT1           : tactic -> tactic
   val REPEAT_FIRST      : (int -> tactic) -> tactic
@@ -65,7 +66,7 @@
   val trace_REPEAT      : bool ref
   val TRY               : tactic -> tactic
   val TRYALL            : (int -> tactic) -> tactic   
-  end;
+end;
 
 
 structure Tactical : TACTICAL = 
@@ -188,6 +189,10 @@
 (*Apply first tactic to 1*)
 fun FIRST1 tacs = FIRST' tacs 1;
 
+(*Apply tactics on consecutive subgoals*)
+fun RANGE [] _ = all_tac
+  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
+
 
 (*** Tracing tactics ***)