# HG changeset patch
# User wenzelm
# Date 1321125249 -3600
# Node ID 6f9e24376ffd577eaef10fa49b4d9108aa708e25
# Parent  b2b087c20e453edf4b29bf316d9c3315bbdc1d15# Parent  f793dd5d84b23a64aa996e5ec19c1cf9d6ba996d
merged

diff -r f793dd5d84b2 -r 6f9e24376ffd src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Sat Nov 12 19:44:56 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Sat Nov 12 20:14:09 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)" 
diff -r f793dd5d84b2 -r 6f9e24376ffd src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Sat Nov 12 19:44:56 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Sat Nov 12 20:14:09 2011 +0100
@@ -276,7 +276,7 @@
   apply auto
   done
 
-lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)";
+lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)"
   unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
 
 lemma bin_nth_bl [rule_format] : "ALL m w. n < m --> 
@@ -717,7 +717,7 @@
   by (induct n)  auto
 
 lemma bl_of_nth_nth_le [rule_format] : "ALL xs. 
-    length xs >= n --> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs";
+    length xs >= n --> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
   apply (induct n, clarsimp)
   apply clarsimp
   apply (rule trans [OF _ hd_Cons_tl])