--- a/src/HOL/Word/Bool_List_Representation.thy Thu Jul 14 14:49:09 2016 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Fri Jul 15 12:23:51 2016 +0200
@@ -9,7 +9,7 @@
section "Bool lists and integers"
theory Bool_List_Representation
-imports Main Bits_Int
+imports Complex_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
done
lemma bin_rsplit_len: