src/HOL/Real.thy
changeset 58061 3d060f43accb
parent 58055 625bdd5c70b2
child 58097 cfd3cff9387b
     1.1 --- a/src/HOL/Real.thy	Thu Aug 28 00:40:38 2014 +0200
     1.2 +++ b/src/HOL/Real.thy	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -2180,10 +2180,10 @@
     1.4  
     1.5  subsection {* Setup for SMT *}
     1.6  
     1.7 -ML_file "Tools/SMT2/smt2_real.ML"
     1.8 -ML_file "Tools/SMT2/z3_new_real.ML"
     1.9 +ML_file "Tools/SMT/smt_real.ML"
    1.10 +ML_file "Tools/SMT/z3_real.ML"
    1.11  
    1.12 -lemma [z3_new_rule]:
    1.13 +lemma [z3_rule]:
    1.14    "0 + (x::real) = x"
    1.15    "x + 0 = x"
    1.16    "0 * x = 0"