changeset 32069 | 6d28bbd33e2c |
parent 31998 | 2c7a24f74db9 |
child 32960 | 69916a850301 |
--- a/src/HOL/Library/Float.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Library/Float.thy Tue Jul 14 16:27:32 2009 +0200 @@ -42,7 +42,7 @@ instance .. end -lemma number_of_float_Float [code_inline, symmetric, code_post]: +lemma number_of_float_Float [code_unfold_post]: "number_of k = Float (number_of k) 0" by (simp add: number_of_float_def number_of_is_id)