# HG changeset patch
# User wenzelm
# Date 1341501535 -7200
# Node ID b7313810b6e6c91d9d135bdeecc23477097b6733
# Parent  3127f9ce52fb4f9e76507c88eb8cba449d3920fe
explicit is better than implicit;

diff -r 3127f9ce52fb -r b7313810b6e6 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Jul 05 16:58:03 2012 +0200
+++ b/src/HOL/Word/Word.thy	Thu Jul 05 17:18:55 2012 +0200
@@ -2344,7 +2344,10 @@
   fixes x' :: "'a::len0 word"
   shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 
 
-lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
+lemma word_ao_equiv:
+  fixes w w' :: "'a::len0 word"
+  shows "(w = w OR w') = (w' = w AND w')"
+  by (auto intro: leoa leao)
 
 lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
   unfolding word_le_def uint_or