Commit 1dcd6400 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Enable from_int for Z3, as suggested by F. Besson.

parent daae53d0
......@@ -132,15 +132,15 @@ theory int.EuclideanDivision
remove prop Div_1
end
(*
theory real.FromInt
syntax function from_int "(from_int %1)"
syntax function from_int "(to_real %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
*)
(*
theory real.Truncate
......
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