328 val th = theory "Float" |
328 val th = theory "Float" |
329 val sg = sign_of th |
329 val sg = sign_of th |
330 |
330 |
331 val float_const = Const ("Float.float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT) |
331 val float_const = Const ("Float.float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT) |
332 |
332 |
333 val float_add_const = Const ("op +", HOLogic.realT --> HOLogic.realT --> HOLogic.realT) |
333 val float_add_const = Const ("HOL.plus", HOLogic.realT --> HOLogic.realT --> HOLogic.realT) |
334 val float_diff_const = Const ("op -", HOLogic.realT --> HOLogic.realT --> HOLogic.realT) |
334 val float_diff_const = Const ("HOL.minus", HOLogic.realT --> HOLogic.realT --> HOLogic.realT) |
335 val float_mult_const = Const ("op *", HOLogic.realT --> HOLogic.realT --> HOLogic.realT) |
335 val float_mult_const = Const ("HOL.times", HOLogic.realT --> HOLogic.realT --> HOLogic.realT) |
336 val float_uminus_const = Const ("uminus", HOLogic.realT --> HOLogic.realT) |
336 val float_uminus_const = Const ("HOL.uminus", HOLogic.realT --> HOLogic.realT) |
337 val float_abs_const = Const ("HOL.abs", HOLogic.realT --> HOLogic.realT) |
337 val float_abs_const = Const ("HOL.abs", HOLogic.realT --> HOLogic.realT) |
338 val float_le_const = Const ("op <=", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT) |
338 val float_le_const = Const ("op <=", HOLogic.realT --> HOLogic.realT --> HOLogic.boolT) |
339 val float_pprt_const = Const ("OrderedGroup.pprt", HOLogic.realT --> HOLogic.realT) |
339 val float_pprt_const = Const ("OrderedGroup.pprt", HOLogic.realT --> HOLogic.realT) |
340 val float_nprt_const = Const ("OrderedGroup.nprt", HOLogic.realT --> HOLogic.realT) |
340 val float_nprt_const = Const ("OrderedGroup.nprt", HOLogic.realT --> HOLogic.realT) |
341 |
341 |