diff --git a/src/plugins/wp/share/ergo/real.PowerReal.mlw b/src/plugins/wp/share/ergo/real.PowerReal.mlw index 97f8c3d547ec82b88e91929a69966f55cf9640ad..140f336820ee45ac74e03671b18c21d22d4c23c3 100644 --- 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)))))) -