| changeset 25062 | af5ef0d4d655 |
| parent 23413 | 5caa2710dd5b |
| child 27435 | b3f8e9bdf9a7 |
--- a/src/HOL/Hyperreal/HDeriv.thy Tue Oct 16 23:12:38 2007 +0200 +++ b/src/HOL/Hyperreal/HDeriv.thy Tue Oct 16 23:12:45 2007 +0200 @@ -369,7 +369,7 @@ subsubsection {* Equivalence of NS and Standard definitions *} -lemma divideR_eq_divide: "x /# y = x / y" +lemma divideR_eq_divide: "x /\<^sub>R y = x / y" by (simp add: real_scaleR_def divide_inverse mult_commute) text{*Now equivalence between NSDERIV and DERIV*}