export ALLGOALS_RANGE;
authorwenzelm
Wed, 08 Mar 2000 17:50:28 +0100
changeset 8366 a70c56d821c7
parent 8365 affb2989d238
child 8367 2d77b5a723f1
export ALLGOALS_RANGE;
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