# HG changeset patch
# User wenzelm
# Date 952534228 -3600
# Node ID a70c56d821c7238e41bba12a9ebd3f16d6835512
# Parent  affb2989d2381274f716acbf311041a62697af81
export ALLGOALS_RANGE;

diff -r affb2989d238 -r a70c56d821c7 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Wed Mar 08 17:49:28 2000 +0100
+++ b/src/Pure/tctical.ML	Wed Mar 08 17:50:28 2000 +0100
@@ -56,6 +56,7 @@
   val suppress_tracing  : bool ref
   val THEN              : tactic * tactic -> tactic
   val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+  val ALLGOALS_RANGE    : (int -> tactic) -> int -> int -> tactic
   val THEN_ALL_NEW	: (int -> tactic) * (int -> tactic) -> int -> tactic
   val REPEAT_ALL_NEW	: (int -> tactic) -> int -> tactic
   val THEN_ELSE         : tactic * (tactic*tactic) -> tactic