Commit 5a0914d6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove some properties already in Coq standard library with the exact same statements.

parent c56d7aaa
......@@ -142,6 +142,10 @@ theory real.Real
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
end
......@@ -150,8 +154,8 @@ theory real.RealInfix
syntax logic (+.) "(%1 + %2)%R"
syntax logic (-.) "(%1 - %2)%R"
syntax logic (-._) "(-%1)%R"
syntax logic ( *.) "(%1 * %2)%R"
syntax logic (/.) "(Rdiv %1 %2)%R"
syntax logic ( *.) "(%1 * %2)%R"
syntax logic (/.) "(%1 / %2)%R"
syntax logic (<=.) "(%1 <= %2)%R"
syntax logic (<.) "(%1 < %2)%R"
......@@ -166,6 +170,8 @@ theory real.Abs
syntax logic abs "(Rabs %1)"
remove prop Abs_pos
end
theory real.FromInt
......@@ -192,6 +198,13 @@ theory real.ExpLog
syntax logic exp "(exp %1)"
syntax logic log "(ln %1)"
remove prop Exp_zero
remove prop Exp_sum
remove prop Log_one
remove prop Log_mul
remove prop Log_exp
remove prop Exp_log
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