changeset 20485 | 3078fd2eec7b |
parent 20217 | 25b068a99d2b |
child 20554 | c433e78d4203 |
--- a/src/HOL/Real/RealDef.thy Wed Sep 06 10:01:27 2006 +0200 +++ b/src/HOL/Real/RealDef.thy Wed Sep 06 13:48:02 2006 +0200 @@ -922,7 +922,7 @@ instance real :: number .. defs (overloaded) - real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)" + real_number_of_def: "(number_of w :: real) == of_int w" --{*the type constraint is essential!*} instance real :: number_ring