src/HOL/Word/Word.thy
changeset 44821 a92f65e174cf
parent 44762 8f9d09241a68
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Word/Word.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -1257,7 +1257,7 @@
     1.4          word_of_int_Ex [of b] 
     1.5          word_of_int_Ex [of c]
     1.6    by (auto simp: word_of_int_hom_syms [symmetric]
     1.7 -                 zadd_0_right add_commute add_assoc add_left_commute
     1.8 +                 add_0_right add_commute add_assoc add_left_commute
     1.9                   mult_commute mult_assoc mult_left_commute
    1.10                   left_distrib right_distrib)
    1.11    
    1.12 @@ -4219,7 +4219,7 @@
    1.13    apply (rule rotater_eqs)
    1.14    apply (simp add: word_size nat_mod_distrib)
    1.15    apply (rule int_eq_0_conv [THEN iffD1])
    1.16 -  apply (simp only: zmod_int zadd_int [symmetric])
    1.17 +  apply (simp only: zmod_int of_nat_add)
    1.18    apply (simp add: rdmods)
    1.19    done
    1.20