src/HOL/Real/Rational.thy

--- a/src/HOL/Real/Rational.thy	Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Thu Sep 25 10:17:22 2008 +0200
@@ -875,6 +875,10 @@
      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':