src/HOL/Real.thy
changeset 56078 624faeda77b5
parent 55945 e96383acecf9
child 56217 dc429a5b13c4
     1.1 --- a/src/HOL/Real.thy	Thu Mar 13 08:56:08 2014 +0100
     1.2 +++ b/src/HOL/Real.thy	Thu Mar 13 13:18:13 2014 +0100
     1.3 @@ -2197,7 +2197,20 @@
     1.4      times_real_inst.times_real uminus_real_inst.uminus_real
     1.5      zero_real_inst.zero_real
     1.6  
     1.7 +
     1.8 +subsection {* Setup for SMT *}
     1.9 +
    1.10  ML_file "Tools/SMT/smt_real.ML"
    1.11  setup SMT_Real.setup
    1.12 +ML_file "Tools/SMT2/smt2_real.ML"
    1.13 +ML_file "Tools/SMT2/z3_new_real.ML"
    1.14 +
    1.15 +lemma [z3_new_rule]:
    1.16 +  "0 + (x::real) = x"
    1.17 +  "x + 0 = x"
    1.18 +  "0 * x = 0"
    1.19 +  "1 * x = x"
    1.20 +  "x + y = y + x"
    1.21 +  by auto
    1.22  
    1.23  end