src/HOL/Tools/SMT/z3_real.ML
changeset 61609 77b453bd616f
parent 60352 d46de31a50c4
child 69204 d5ab1636660b
     1.1 --- a/src/HOL/Tools/SMT/z3_real.ML	Tue Nov 03 11:20:21 2015 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_real.ML	Tue Nov 10 14:18:41 2015 +0000
     1.3 @@ -13,14 +13,14 @@
     1.4  fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i)
     1.5    | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
     1.6        SOME (@{term "Rings.divide :: real => _"} $ t1 $ t2)
     1.7 -  | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t)
     1.8 +  | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Int.of_int :: int => _"} $ t)
     1.9    | real_term_parser _ = NONE
    1.10  
    1.11  fun abstract abs t =
    1.12    (case t of
    1.13      (c as @{term "Rings.divide :: real => _"}) $ t1 $ t2 =>
    1.14        abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
    1.15 -  | (c as @{term "Real.real :: int => _"}) $ t =>
    1.16 +  | (c as @{term "Int.of_int :: int => _"}) $ t =>
    1.17        abs t #>> (fn u => SOME (c $ u))
    1.18    | _ => pair NONE)
    1.19