Change provable new axiom to lemma

052959ac · Raphael Rieu-Helft · 8c1a6b32 · 052959ac
Commit 052959ac authored Feb 14, 2018 by Raphael Rieu-Helft
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

stdlib/real.mlw stdlib/real.mlw +1 -1

No files found.
--- a/stdlib/real.mlw
+++ b/stdlib/real.mlw
@@ -128,7 +128,7 @@ module FromInt
  axiom Neg:
    forall x:int. from_int (Int.(-_) (x)) = - from_int x

-  axiom Injective:
+  lemma Injective:
    forall x y: int. from_int x = from_int y -> x = y
  axiom Monotonic:
    forall x y:int. Int.(<=) x y -> from_int x <= from_int y