src/HOL/Word/Bool_List_Representation.thy
changeset 45475 b2b087c20e45
parent 44939 5930d35c976d
child 45543 827bf668c822
--- 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])