src/HOL/Library/Float.thy
changeset 53215 5e47c31c6f7c
parent 51542 738598beeb26
child 53381 355a4cac5440
     1.1 --- a/src/HOL/Library/Float.thy	Mon Aug 26 23:39:53 2013 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Aug 27 14:37:56 2013 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4      and real_of_float_max: "real (max x y) = max (real x) (real y)"
     1.5    by (simp_all add: min_def max_def)
     1.6  
     1.7 -instance float :: dense_linorder
     1.8 +instance float :: unbounded_dense_linorder
     1.9  proof
    1.10    fix a b :: float
    1.11    show "\<exists>c. a < c"