src/HOL/Real/Rational.thy

      else if d = 0
        then a = 0 \<or> b = 0
      else a * d =  b * c)"
   by (auto simp add: eq eq_rat)
 
+lemma rat_eq_refl [code nbe]:
+  "eq_class.eq (r::rat) r \<longleftrightarrow> True"
+  by (rule HOL.eq_refl)
+
 end
 
 lemma le_rat':
   assumes "b \<noteq> 0"
     and "d \<noteq> 0"