src/HOL/Tools/SMT/smt_real.ML
changeset 40579 98ebd2300823
parent 40516 516a367eb38c
child 41059 d2b1fc1b8e19
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed Nov 17 08:14:55 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Nov 17 08:14:56 2010 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  (* Z3 builtins *)
     1.5  
     1.6  local
     1.7 -  fun z3_builtin_fun @{term "op / :: real => _"} ts = SOME ("/", ts)
     1.8 +  fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
     1.9      | z3_builtin_fun _ _ = NONE
    1.10  in
    1.11  
    1.12 @@ -86,13 +86,13 @@
    1.13      if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
    1.14      else NONE
    1.15  
    1.16 -  val mk_uminus = Thm.capply @{cterm "uminus :: real => _"}
    1.17 -  val mk_add = Thm.mk_binop @{cterm "op + :: real => _"}
    1.18 -  val mk_sub = Thm.mk_binop @{cterm "op - :: real => _"}
    1.19 -  val mk_mul = Thm.mk_binop @{cterm "op * :: real => _"}
    1.20 -  val mk_div = Thm.mk_binop @{cterm "op / :: real => _"}
    1.21 -  val mk_lt = Thm.mk_binop @{cterm "op < :: real => _"}
    1.22 -  val mk_le = Thm.mk_binop @{cterm "op <= :: real => _"}
    1.23 +  val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
    1.24 +  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
    1.25 +  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
    1.26 +  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
    1.27 +  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
    1.28 +  val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
    1.29 +  val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
    1.30  
    1.31    fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    1.32      | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)