# HG changeset patch
# User haftmann
# Date 1282136110 -7200
# Node ID f2709bc1e41f07357d4063c63481898ddccac1e9
# Parent  a9ce311eb6b98f03259a9246ecf7c4fc493fb4be
moved spurious auxiliary lemma here

diff -r a9ce311eb6b9 -r f2709bc1e41f src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Aug 18 14:55:10 2010 +0200
+++ b/src/HOL/Word/Word.thy	Wed Aug 18 14:55:10 2010 +0200
@@ -4034,6 +4034,11 @@
   "length (rotater n xs) = length xs"
   by (simp add : rotater_rev)
 
+lemma restrict_to_left:
+  assumes "x = y"
+  shows "(x = z) = (y = z)"
+  using assms by simp
+
 lemmas rrs0 = rotate_eqs [THEN restrict_to_left, 
   simplified rotate_gal [symmetric] rotate_gal' [symmetric], standard]
 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]