diff -r 98af01f897c9 -r b2b087c20e45 src/HOL/Word/Bit_Int.thy --- a/src/HOL/Word/Bit_Int.thy Fri Nov 11 22:09:07 2011 +0100 +++ b/src/HOL/Word/Bit_Int.thy Sat Nov 12 13:01:56 2011 +0100 @@ -357,7 +357,7 @@ done lemmas int_and_le = - xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] ; + xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] lemma bin_nth_ops: "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"