--- a/src/HOL/Word/Bool_List_Representation.thy Sun Nov 13 21:37:30 2016 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Sat Nov 19 19:43:09 2016 +0100
@@ -9,7 +9,7 @@
section "Bool lists and integers"
theory Bool_List_Representation
-imports Complex_Main Bits_Int
+imports Main Bits_Int
begin
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
@@ -1106,7 +1106,7 @@
apply (case_tac m)
apply simp
apply (case_tac "m <= n")
- apply auto
+ apply (auto simp add: div_add_self2)
done
lemma bin_rsplit_len: