src/HOL/Library/Abstract_Rat.thy
changeset 30042 31039ee583fa
parent 29667 53103fc8ffa3
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Sat Feb 21 09:58:45 2009 +0100
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Sat Feb 21 20:52:30 2009 +0100
     1.3 @@ -247,7 +247,7 @@
     1.4      (of_int(n div d)::'a::{field, ring_char_0}) = of_int n / of_int d"
     1.5    apply (frule of_int_div_aux [of d n, where ?'a = 'a])
     1.6    apply simp
     1.7 -  apply (simp add: zdvd_iff_zmod_eq_0)
     1.8 +  apply (simp add: dvd_eq_mod_eq_0)
     1.9  done
    1.10  
    1.11