# HG changeset patch
# User huffman
# Date 1321099316 -3600
# Node ID b2b087c20e453edf4b29bf316d9c3315bbdc1d15
# Parent  98af01f897c98de7cf455063c18977bf7c70e673
removed some old-style semicolons

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)" 
diff -r 98af01f897c9 -r b2b087c20e45 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Nov 11 22:09:07 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Sat Nov 12 13:01:56 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])