Commit 942829fd authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix axiom that states 0.0 ^ (-1) = 0.0 in real.PowerReal theory.

Remove the incorrect Coq realization of PowerReal.pow by Rpower, since the
latter is only meaningfully defined for positive first arguments, e.g.
Rpower (-1) 3 = 1!
parent b003c3a7
......@@ -274,15 +274,6 @@ theory real.PowerInt
(* remove prop Power_sum *) (* not the same as powerRZ_add *)
(* remove prop Power_mult *)
end
theory real.PowerReal
prelude "Require Import Rpower."
syntax function pow "(Rpower %1 %2)"
end
theory real.Trigonometry
......
......@@ -253,7 +253,7 @@ theory PowerReal
function pow real real : real
axiom Pow_zero_y:
forall y:real. y <> 0.0 -> pow 0.0 y = 0.0
forall y:real. y > 0.0 -> pow 0.0 y = 0.0
axiom Pow_x_zero:
forall x:real. x <> 0.0 -> pow x 0.0 = 1.0
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment