src/HOL/Tools/SMT/z3_real.ML
changeset 60352 d46de31a50c4
parent 58061 3d060f43accb
child 61609 77b453bd616f
     1.1 --- a/src/HOL/Tools/SMT/z3_real.ML	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_real.ML	Mon Jun 01 18:59:21 2015 +0200
     1.3 @@ -12,13 +12,13 @@
     1.4  
     1.5  fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number @{typ Real.real} i)
     1.6    | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
     1.7 -      SOME (@{term "inverse_class.divide :: real => _"} $ t1 $ t2)
     1.8 +      SOME (@{term "Rings.divide :: real => _"} $ t1 $ t2)
     1.9    | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (@{term "Real.real :: int => _"} $ t)
    1.10    | real_term_parser _ = NONE
    1.11  
    1.12  fun abstract abs t =
    1.13    (case t of
    1.14 -    (c as @{term "inverse_class.divide :: real => _"}) $ t1 $ t2 =>
    1.15 +    (c as @{term "Rings.divide :: real => _"}) $ t1 $ t2 =>
    1.16        abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
    1.17    | (c as @{term "Real.real :: int => _"}) $ t =>
    1.18        abs t #>> (fn u => SOME (c $ u))