theory Real imports RComplete RealVector uses "Tools/SMT/smt_real.ML" begin setup {* SMT_Real.setup *} end