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 Nov 19 19:43:09 2016 +0100 (2016-11-19)
changeset 64507eace715f4988
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
     1.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Sun Nov 13 21:37:30 2016 +0100
     1.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Sat Nov 19 19:43:09 2016 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  section "Bool lists and integers"
     1.5  
     1.6  theory Bool_List_Representation
     1.7 -imports Complex_Main Bits_Int
     1.8 +imports Main Bits_Int
     1.9  begin
    1.10  
    1.11  definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    1.12 @@ -1106,7 +1106,7 @@
    1.13    apply (case_tac m)
    1.14    apply simp
    1.15    apply (case_tac "m <= n")
    1.16 -   apply auto
    1.17 +   apply (auto simp add: div_add_self2)
    1.18    done
    1.19  
    1.20  lemma bin_rsplit_len: