src/HOL/Real/Float.ML
changeset 16828 581764860c2b
parent 16782 b214f21ae396
child 16873 9ed940a1bebb
equal deleted inserted replaced
16827:c90a1f450327 16828:581764860c2b
    14     val approx_dec_by_bin : IntInf.int -> floatrep -> floatrep * floatrep
    14     val approx_dec_by_bin : IntInf.int -> floatrep -> floatrep * floatrep
    15     val approx_decstr_by_bin : int -> string -> floatrep * floatrep
    15     val approx_decstr_by_bin : int -> string -> floatrep * floatrep
    16 end 
    16 end 
    17 =
    17 =
    18 struct
    18 struct
    19 
       
    20 fun fst (a,b) = a
       
    21 fun snd (a,b) = b
       
    22 
       
    23 val filter = List.filter;
       
    24 
    19 
    25 exception Destruct_floatstr of string;
    20 exception Destruct_floatstr of string;
    26 
    21 
    27 fun destruct_floatstr isDigit isExp number = 
    22 fun destruct_floatstr isDigit isExp number = 
    28     let
    23     let