diff r 28fa57b57209 r 34264f5e4691 src/HOL/Real/RealDef.thy
 a/src/HOL/Real/RealDef.thy Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Real/RealDef.thy Thu Jul 01 12:29:53 2004 +0200
@@ 732,25 +732,12 @@
instance real :: number ..
primrec (*the type constraint is essential!*)
 number_of_Pls: "number_of bin.Pls = 0"
 number_of_Min: "number_of bin.Min =  (1::real)"
 number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
 (number_of w) + (number_of w)"

declare number_of_Pls [simp del]
 number_of_Min [simp del]
 number_of_BIT [simp del]
+defs (overloaded)
+ real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)"
+ {*the type constraint is essential!*}
instance real :: number_ring
proof
 show "Numeral0 = (0::real)" by (rule number_of_Pls)
 show "1 =  (1::real)" by (rule number_of_Min)
 fix w :: bin and x :: bool
 show "(number_of (w BIT x) :: real) =
 (if x then 1 else 0) + number_of w + number_of w"
 by (rule number_of_BIT)
qed
+by (intro_classes, simp add: real_number_of_def)
text{*Collapse applications of @{term real} to @{term number_of}*}