src/HOL/RComplete.thy
changeset 37887 2ae085b07f2f
parent 36979 da7c06ab3169
child 41550 efa734d9b221
     1.1 --- a/src/HOL/RComplete.thy	Mon Jul 19 16:09:44 2010 +0200
     1.2 +++ b/src/HOL/RComplete.thy	Mon Jul 19 16:09:44 2010 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4    have "x = y-(y-x)" by simp
     1.5    also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
     1.6    also have "\<dots> = real p / real q"
     1.7 -    by (simp only: inverse_eq_divide diff_def real_of_nat_Suc 
     1.8 +    by (simp only: inverse_eq_divide diff_minus real_of_nat_Suc 
     1.9      minus_divide_left add_divide_distrib[THEN sym]) simp
    1.10    finally have "x<r" by (unfold r_def)
    1.11    have "p<Suc p" .. also note main[THEN sym]