improved PVS driver

parent e3f873cb
......@@ -109,7 +109,6 @@ theory int.MinMax
end
theory real.Real
syntax function zero "0"
......@@ -119,10 +118,7 @@ theory real.Real
syntax function ( - ) "(%1 - %2)"
syntax function (-_) "(-%1)"
syntax function ( * ) "(%1 * %2)"
(*
syntax function ( / ) "(%1 / %2)"
syntax function inv "(1 / %1)"
*)
(* / and inv are defined in the realization *)
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
......@@ -171,7 +167,8 @@ theory real.RealInfix
syntax function (-.) "(%1 - %2)"
syntax function (-._) "(-%1)"
syntax function ( *.) "(%1 * %2)"
(* syntax function (/.) "(%1 / %2)" *)
syntax function (/.) "real@Real.infix_sl(%1, %2)"
syntax function inv "real@Real.inv(%1)"
syntax predicate (<=.) "(%1 <= %2)"
syntax predicate (<.) "(%1 < %2)"
......
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