1.1 --- a/src/HOL/Real/Rational.thy	Fri Jul 25 12:03:32 2008 +0200
     1.2 +++ b/src/HOL/Real/Rational.thy	Fri Jul 25 12:03:34 2008 +0200
     1.3 @@ -436,8 +436,8 @@
     1.4    next
     1.5      show "q \<le> q"
     1.6        by (induct q) simp
     1.7 -    show "(q < r) = (q \<le> r \<and> q \<noteq> r)"
     1.8 -      by (simp only: less_rat_def)
     1.9 +    show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)"
    1.10 +      by (induct q, induct r) (auto simp add: le_less mult_commute)
    1.11      show "q \<le> r \<or> r \<le> q"
    1.12        by (induct q, induct r)
    1.13           (simp add: mult_commute, rule linorder_linear)