[wp] fix unecessary int-power

445a43f3 · Loïc Correnson · François Bobot · 036d849b · 445a43f3
Commit 445a43f3 authored 5 years ago by Loïc Correnson Committed by François Bobot 5 years ago
--- a/src/plugins/wp/share/ergo/real.PowerReal.mlw
+++ b/src/plugins/wp/share/ergo/real.PowerReal.mlw
@@ -48,8 +48,3 @@ axiom Pow_one_y : (forall y:real. (pow(1.0, y) = 1.0))
 axiom Pow_x_two : (forall x:real. ((0.0 <  x) -> (pow(x, 2.0) = sqr(x))))

 axiom Pow_half : (forall x:real. ((0.0 <  x) -> (pow(x, 0.5) = sqrt(x))))
-
-axiom pow_from_int :
-  (forall x:int. forall y:int. ((0 <  x) -> ((0 <= y) -> (pow(from_int(x),
-  from_int(y)) = from_int(power(x, y))))))
-