src/HOL/Word/Bit_Int.thy
changeset 45475 b2b087c20e45
parent 44939 5930d35c976d
child 45529 0e1037d4e049
--- 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)"