File ‹Tools/SMT/z3_real.ML›

(*  Title:      HOL/Tools/SMT/z3_real.ML
    Author:     Sascha Boehme, TU Muenchen

Z3 setup for reals  based on a relaxed version of SMT-LIB (outside of LIRA).
*)

structure Z3_Real: sig end =
struct

val setup_builtins =
  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
    (\<^Const>‹times \<^Type>‹real››, "*") #>
  SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
    (\<^Const>‹divide \<^Type>‹real››, "/")


val _ = Theory.setup (Context.theory_map
  setup_builtins)

end;