src/HOL/Word/Bool_List_Representation.thy

   apply (cut_tac x=n and y="size list" in linorder_less_linear)
   apply (erule disjE, simp add: nth_append)+
   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 --> 
     bin_nth w n = nth (rev (bin_to_bl m w)) n"
   apply (induct n)

 lemma bl_of_nth_inj: 
   "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
   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])
    apply (frule Suc_le_lessD)
    apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])