Commit 2e456272 authored by MARCHE Claude's avatar MARCHE Claude

theory real.RealInfix: reintroduced symbol inv which was used in PVS driver

parent 3e94b5fb
......@@ -58,9 +58,7 @@ theory RealInfix
let function ( *.) (x:real) (y:real) : real = x * y
function (/.) (x:real) (y:real) : real = x / y
let function (-._) (x:real) : real = - x
(***
let function inv (x:real) : real = Real.inv x
*)
function inv (x:real) : real = Real.inv x
let predicate (<=.) (x:real) (y:real) = x <= y
let predicate (>=.) (x:real) (y:real) = 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