src/HOL/Library/Float.thy
changeset 49812 e3945ddcb9aa
parent 47937 70375fa2679d
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Library/Float.thy	Wed Oct 10 16:41:19 2012 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Wed Oct 10 17:43:23 2012 +0200
     1.3 @@ -9,9 +9,11 @@
     1.4  imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
     1.5  begin
     1.6  
     1.7 -typedef float = "{m * 2 powr e | (m :: int) (e :: int). True }"
     1.8 +definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
     1.9 +
    1.10 +typedef (open) float = float
    1.11    morphisms real_of_float float_of
    1.12 -  by auto
    1.13 +  unfolding float_def by auto
    1.14  
    1.15  defs (overloaded)
    1.16    real_of_float_def[code_unfold]: "real \<equiv> real_of_float"