# HG changeset patch
# User wenzelm
# Date 1479580989 -3600
# Node ID eace715f498830536257e57a9d141732cfc123e2
# Parent  b3ccfd59097d1bac596848bc09ac4083e973cea9
avoid import of Complex_Main into Word library (amending 34b7e2da95f6), e.g. to avoid intrusion of const "ii" into theories without complex numbers;

diff -r b3ccfd59097d -r eace715f4988 src/HOL/Word/Bool_List_Representation.thy
--- 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: