equal
deleted
inserted
replaced
202 in |
202 in |
203 approx_dec_by_bin n (q,r) |
203 approx_dec_by_bin n (q,r) |
204 end |
204 end |
205 |
205 |
206 fun mk_float (a, b) = @{term "float"} $ |
206 fun mk_float (a, b) = @{term "float"} $ |
207 HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b)); |
207 HOLogic.mk_prod (apply2 (HOLogic.mk_number HOLogic.intT) (a, b)); |
208 |
208 |
209 fun dest_float (Const (@{const_name float}, _) $ (Const (@{const_name Pair}, _) $ a $ b)) = |
209 fun dest_float (Const (@{const_name float}, _) $ (Const (@{const_name Pair}, _) $ a $ b)) = |
210 pairself (snd o HOLogic.dest_number) (a, b) |
210 apply2 (snd o HOLogic.dest_number) (a, b) |
211 | dest_float t = ((snd o HOLogic.dest_number) t, 0); |
211 | dest_float t = ((snd o HOLogic.dest_number) t, 0); |
212 |
212 |
213 fun approx_float prec f value = |
213 fun approx_float prec f value = |
214 let |
214 let |
215 val interval = approx_decstr_by_bin prec value |
215 val interval = approx_decstr_by_bin prec value |