summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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]