diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Real/Float.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -11,9 +11,11 @@
 begin
 
 definition
-  pow2 :: "int \<Rightarrow> real"
+  pow2 :: "int \<Rightarrow> real" where
   "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
-  float :: "int * int \<Rightarrow> real"
+
+definition
+  float :: "int * int \<Rightarrow> real" where
   "float x = real (fst x) * pow2 (snd x)"
 
 lemma pow2_0[simp]: "pow2 0 = 1"
@@ -99,9 +101,11 @@
 by (simp add: float_def ring_eq_simps)
 
 definition
-  int_of_real :: "real \<Rightarrow> int"
+  int_of_real :: "real \<Rightarrow> int" where
   "int_of_real x = (SOME y. real y = x)"
-  real_is_int :: "real \<Rightarrow> bool"
+
+definition
+  real_is_int :: "real \<Rightarrow> bool" where
   "real_is_int x = (EX (u::int). x = real u)"
 
 lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"