--- 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}*}