Commit cd022a50 authored by Piotr Trojanek's avatar Piotr Trojanek Committed by Stefan Berghofer
Browse files

include Isabelle reals in main realization file

Realization of theory of reals needs to be included in the main realization
file, so it is visible by default when proving VCs in Isabelle.
parent 74246162
......@@ -7,6 +7,7 @@ imports
Why3_Bool
Why3_Number
Why3_BV
Why3_Real
begin
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