Commit faeb75b4 authored by MARCHE Claude's avatar MARCHE Claude

Metitarski driver: a small additional improvement

parent 01efbbd2
......@@ -72,6 +72,10 @@ theory real.Real
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
(* These follow from Metitarski's axioms. *)
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
......
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