src/HOL/Decision_Procs/approximation_generator.ML
 changeset 64519 51be997d0698 parent 63931 f17a1c60ac39 child 69597 ff784d5a5bfb
equal inserted replaced
64518:b87697eec2ac 64519:51be997d0698
`    50   | mapprox_floatarith (@{term Min} \$ a \$ b) xs =`
`    50   | mapprox_floatarith (@{term Min} \$ a \$ b) xs =`
`    51       Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs)`
`    51       Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs)`
`    52   | mapprox_floatarith @{term Pi} _ = Math.pi`
`    52   | mapprox_floatarith @{term Pi} _ = Math.pi`
`    53   | mapprox_floatarith (@{term Sqrt} \$ a) xs = Math.sqrt (mapprox_floatarith a xs)`
`    53   | mapprox_floatarith (@{term Sqrt} \$ a) xs = Math.sqrt (mapprox_floatarith a xs)`
`    54   | mapprox_floatarith (@{term Exp} \$ a) xs = Math.exp (mapprox_floatarith a xs)`
`    54   | mapprox_floatarith (@{term Exp} \$ a) xs = Math.exp (mapprox_floatarith a xs)`
`       `
`    55   | mapprox_floatarith (@{term Powr} \$ a \$ b) xs =`
`       `
`    56       Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)`
`    55   | mapprox_floatarith (@{term Ln} \$ a) xs = Math.ln (mapprox_floatarith a xs)`
`    57   | mapprox_floatarith (@{term Ln} \$ a) xs = Math.ln (mapprox_floatarith a xs)`
`    56   | mapprox_floatarith (@{term Power} \$ a \$ n) xs =`
`    58   | mapprox_floatarith (@{term Power} \$ a \$ n) xs =`
`    57       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))`
`    59       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))`
`    58   | mapprox_floatarith (@{term Floor} \$ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))`
`    60   | mapprox_floatarith (@{term Floor} \$ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))`
`    59   | mapprox_floatarith (@{term Var} \$ n) xs = nth xs (nat_of_term n)`
`    61   | mapprox_floatarith (@{term Var} \$ n) xs = nth xs (nat_of_term n)`