src/HOL/Word/Word.thy
changeset 64243 aee949f6642d
parent 64242 93c6f0da5c70
child 64593 50c715579715
     1.1 --- a/src/HOL/Word/Word.thy	Sun Oct 16 09:31:05 2016 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Sun Oct 16 09:31:05 2016 +0200
     1.3 @@ -3867,7 +3867,7 @@
     1.4     apply clarsimp
     1.5    apply (clarsimp simp add : nth_append size_rcat_lem)
     1.6    apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
     1.7 -         td_gal_lt_len less_Suc_eq_le div_mult_mod_eq')
     1.8 +         td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
     1.9    apply clarsimp
    1.10    done
    1.11