equal
deleted
inserted
replaced
65 |
65 |
66 fun z3_mk_builtin_num _ i T = |
66 fun z3_mk_builtin_num _ i T = |
67 if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) |
67 if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) |
68 else NONE |
68 else NONE |
69 |
69 |
70 val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)}) |
70 val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)}) |
71 val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)}) |
71 val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)}) |
72 val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) |
72 val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) |
73 val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) |
73 val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) |
74 val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) |
74 val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) |
75 val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) |
75 val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) |