--- a/src/HOL/Decision_Procs/approximation_generator.ML Mon Nov 21 14:49:52 2016 +0100
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Mon Nov 21 15:30:35 2016 +0100
@@ -52,6 +52,8 @@
| mapprox_floatarith @{term Pi} _ = Math.pi
| mapprox_floatarith (@{term Sqrt} $ a) xs = Math.sqrt (mapprox_floatarith a xs)
| mapprox_floatarith (@{term Exp} $ a) xs = Math.exp (mapprox_floatarith a xs)
+ | mapprox_floatarith (@{term Powr} $ a $ b) xs =
+ Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)
| mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs)
| mapprox_floatarith (@{term Power} $ a $ n) xs =
Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))