correct mistake in big_float_is_int axiom

9951e364 · Clément Fumex · 9ab5761b · 9951e364
Commit 9951e364 authored Nov 29, 2016 by Clément Fumex
--- a/theories/ieee_float.why
+++ b/theories/ieee_float.why
@@ -653,7 +653,7 @@ theory GenericFloat
  (** big floats are ints *)
  axiom big_float_is_int: forall m i.
    is_finite i ->
-    (i .<= (of_int m (- max_representable_integer)) /\
+    (i .<= (of_int m (- max_representable_integer)) \/
    (of_int m max_representable_integer) .<= i) ->
      is_int i