avoid import of Complex_Main into Word library (amending 34b7e2da95f6), e.g. to avoid intrusion of const "ii" into theories without complex numbers;
authorwenzelm
Sat, 19 Nov 2016 19:43:09 +0100
changeset 64507 eace715f4988
parent 64506 b3ccfd59097d
child 64508 874555896035
avoid import of Complex_Main into Word library (amending 34b7e2da95f6), e.g. to avoid intrusion of const "ii" into theories without complex numbers;
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: