# HG changeset patch
# User nipkow
# Date 806945093 -7200
# Node ID 03dc596b3a18b45ff54376b2a29e9b18d95d5d1a
# Parent  bc3093616ba4fc1941a85f111cabd8711dbd2308
added rotate_tac.

diff -r bc3093616ba4 -r 03dc596b3a18 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Fri Jul 28 17:21:44 1995 +0200
+++ b/src/Pure/tactic.ML	Fri Jul 28 17:24:53 1995 +0200
@@ -71,6 +71,7 @@
   val rewrite_goals_tac: thm list -> tactic
   val rewrite_tac: thm list -> tactic
   val rewtac: thm -> tactic
+  val rotate_tac: int -> int -> tactic
   val rtac: thm -> int -> tactic
   val rule_by_tactic: tactic -> thm -> thm
   val subgoal_tac: string -> int -> tactic
@@ -469,5 +470,14 @@
 (*Prunes all redundant parameters from the proof state by rewriting*)
 val prune_params_tac = rewrite_tac [triv_forall_equality];
 
+(* rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
+ * right to left if n is positive, and from left to right if n is negative.
+ *)
+fun rotate_tac n =
+  let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
+  in if n >= 0 then rot n
+     else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i)
+  end;
+
 end;
 end;