| changeset 25762 | c03e9d04b3e4 |
| parent 25571 | c9e39eafc7a0 |
| child 25885 | 6fbc3f54f819 |
--- a/src/HOL/Real/RealDef.thy Wed Jan 02 12:22:38 2008 +0100 +++ b/src/HOL/Real/RealDef.thy Wed Jan 02 15:14:02 2008 +0100 @@ -25,7 +25,7 @@ real_of_preal :: "preal => real" where "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})" -instantiation real :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}" +instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}" begin definition