src/HOL/Tools/SMT/smt_real.ML
changeset 41072 9f9bc1bdacef
parent 41059 d2b1fc1b8e19
child 41280 a7de9d36f4f2
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Tue Dec 07 21:58:36 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Dec 08 08:33:02 2010 +0100
     1.3 @@ -106,9 +106,9 @@
     1.4  (* setup *)
     1.5  
     1.6  val setup =
     1.7 -  setup_builtins #>
     1.8    Context.theory_map (
     1.9      SMTLIB_Interface.add_logic (10, smtlib_logic) #>
    1.10 +    setup_builtins #>
    1.11      Z3_Interface.add_mk_builtins z3_mk_builtins #>
    1.12      fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
    1.13      Z3_Proof_Tools.add_simproc real_linarith_proc)