src/HOL/Word/Bit_Representation.thy
changeset 58834 773b378d9313
parent 58645 94bef115c08f
child 58874 7172c7ffb047
     1.1 --- a/src/HOL/Word/Bit_Representation.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -316,8 +316,7 @@
     1.4    apply (clarsimp simp: mod_mult_mult1 [symmetric] 
     1.5           zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
     1.6    apply (rule trans [symmetric, OF _ emep1])
     1.7 -     apply auto
     1.8 -  apply (auto simp: even_iff_mod_2_eq_zero)
     1.9 +  apply auto
    1.10    done
    1.11  
    1.12  subsection "Simplifications for (s)bintrunc"