src/HOL/Library/Float.thy
changeset 31998 2c7a24f74db9
parent 31863 e391eee8bf14
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/Library/Float.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    "of_float (Float a b) = real a * pow2 b"
     1.5  
     1.6  defs (overloaded)
     1.7 -  real_of_float_def [code unfold]: "real == of_float"
     1.8 +  real_of_float_def [code_unfold]: "real == of_float"
     1.9  
    1.10  primrec mantissa :: "float \<Rightarrow> int" where
    1.11    "mantissa (Float a b) = a"
    1.12 @@ -42,7 +42,7 @@
    1.13  instance ..
    1.14  end
    1.15  
    1.16 -lemma number_of_float_Float [code inline, symmetric, code post]:
    1.17 +lemma number_of_float_Float [code_inline, symmetric, code_post]:
    1.18    "number_of k = Float (number_of k) 0"
    1.19    by (simp add: number_of_float_def number_of_is_id)
    1.20