# HG changeset patch
# User immler
# Date 1479738635 -3600
# Node ID 51be997d0698583bf2d3f5a99f37381a146d3a6c
# Parent  b87697eec2acb383b204d4874c9d8f9c25823fc1
op powr for quickcheck[approximation] (amending 67792e4a5486)

diff -r b87697eec2ac -r 51be997d0698 src/HOL/Decision_Procs/approximation_generator.ML
--- 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))