Commit db5dfead authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

a typo in real.Abs (who's to be blamed?)

parent 4a808fcd
......@@ -21,7 +21,7 @@ theory Abs
use import Real
logic abs(real) : real = if x >= 0.0 then x else -x
logic abs(x : real) : real = if x >= 0.0 then x else -x
lemma Abs_le: forall x,y:real. abs(x) <= y <-> -y <= x <= y
......
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