You should always have success by unfolding powr_def. And I’m told that the necessary changes to “approximation” are not difficult.
Larry > On 12 Apr 2015, at 12:26, Manuel Eberl <ebe...@in.tum.de> wrote: > > I am not terribly happy about that. I use approximation of powr in my work on > Akra–Bazzi and the Master theorem. > > I take it that a powr b = exp (ln a * b) still holds for positive a. I could > probably apply that rewrite rule before applying approximation, but it would > of course be nice if I did not have to. > > The issue is, however, not terribly urgent since my project is still several > weeks from being finished, and I only need approximation for a small part > that is independent from everything else. > > Manuel > > Larry Paulson <l...@cam.ac.uk> wrote: > >>> * Complex powers and square roots. The functions "ln" and "powr" are now >>> overloaded for types real and complex, and 0 powr y = 0 by definition. >>> INCOMPATIBILITY: type constraints may be necessary. >> >> But I had to remove support for powr in code generation and the >> approximation method. If anybody thinks these are priorities for >> restoration, I guess we only have a few days. The problem with code >> generation has something to do with types. >> >> Larry >> >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
