src/HOL/Rational.thy
changeset 29925 17d1e32ef867
parent 29880 3dee8ff45d3d
child 29940 83b373f61d41
     1.1 --- a/src/HOL/Rational.thy	Sun Feb 15 16:25:39 2009 +0100
     1.2 +++ b/src/HOL/Rational.thy	Sun Feb 15 22:58:02 2009 +0100
     1.3 @@ -801,7 +801,7 @@
     1.4    then have "?c \<noteq> 0" by simp
     1.5    then have "Fract ?c ?c = Fract 1 1" by (simp add: eq_rat)
     1.6    moreover have "Fract (a div ?c * ?c + a mod ?c) (b div ?c * ?c + b mod ?c) = Fract a b"
     1.7 -   by (simp add: semiring_div_class.mod_div_equality)
     1.8 +    by (simp add: semiring_div_class.mod_div_equality)
     1.9    moreover have "a mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
    1.10    moreover have "b mod ?c = 0" by (simp add: dvd_eq_mod_eq_0 [symmetric])
    1.11    ultimately show ?thesis