Commit 6895bbd3 authored by MARCHE Claude's avatar MARCHE Claude

removed lemmas that cause regression

parent d15da6d4
......@@ -33,7 +33,9 @@ theory Group
axiom Inv_def : forall x:t. op x (inv x) = unit
(*
lemma Inv_unit : forall x y:t. op x (inv y) = unit -> x = y
*)
end
......
......@@ -23,7 +23,9 @@ theory Abs
lemma Abs_pos: forall x:int. abs x >= 0
(*
lemma Abs_zero: forall x:int. abs x = 0 -> x = 0
*)
end
......
......@@ -11,7 +11,9 @@ theory Real
clone export algebra.OrderedField with type t = real,
function zero = zero, function one = one, predicate (<=) = (<=)
(*
lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y
*)
end
......@@ -42,7 +44,9 @@ theory Abs
lemma Abs_pos: forall x:real. abs x >= 0.0
(*
lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0
*)
end
......
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