| changeset 45051 | c478d1876371 |
| parent 44633 | 8a2fd7418435 |
| child 46783 | 3e89a5cab8d7 |
--- a/src/HOL/Import/HOLLightReal.thy Thu Sep 22 13:17:14 2011 -0700 +++ b/src/HOL/Import/HOLLightReal.thy Thu Sep 22 14:12:16 2011 -0700 @@ -233,7 +233,7 @@ lemma REAL_SUB_INV: "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)" - by (simp add: division_ring_inverse_diff real_divide_def) + by (simp add: division_ring_inverse_diff divide_real_def) lemma REAL_DOWN: "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"