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