| changeset 15234 | ec91a90c604e |
| parent 15229 | 1eb23f805c06 |
| child 15413 | 901d1bfedf09 |
--- a/src/HOL/Hyperreal/HyperDef.thy Wed Oct 06 13:59:33 2004 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Thu Oct 07 15:42:30 2004 +0200 @@ -506,9 +506,7 @@ qed lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" -apply auto -apply (rule OrderedGroup.add_right_cancel [of _ "-y", THEN iffD1], auto) -done +by auto lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" by auto