--- a/src/HOL/Library/Float.thy Tue Jul 14 10:53:44 2009 +0200
+++ b/src/HOL/Library/Float.thy Tue Jul 14 10:54:04 2009 +0200
@@ -19,7 +19,7 @@
"of_float (Float a b) = real a * pow2 b"
defs (overloaded)
- real_of_float_def [code unfold]: "real == of_float"
+ real_of_float_def [code_unfold]: "real == of_float"
primrec mantissa :: "float \<Rightarrow> int" where
"mantissa (Float a b) = a"
@@ -42,7 +42,7 @@
instance ..
end
-lemma number_of_float_Float [code inline, symmetric, code post]:
+lemma number_of_float_Float [code_inline, symmetric, code_post]:
"number_of k = Float (number_of k) 0"
by (simp add: number_of_float_def number_of_is_id)