equal
deleted
inserted
replaced
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) |