# 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')) \ (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