src/HOL/Number_Theory/Residues.thy
changeset 36350 bc7982c54e37
parent 35416 d8d7d1b785af
child 41541 1fa4725c4656
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Apr 26 11:34:17 2010 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Apr 26 11:34:19 2010 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4    apply (subst mod_add_eq [symmetric])
     1.5    apply (subst mult_commute)
     1.6    apply (subst zmod_zmult1_eq [symmetric])
     1.7 -  apply (simp add: ring_simps)
     1.8 +  apply (simp add: field_simps)
     1.9  done
    1.10  
    1.11  end