[isabelle-dev] Regression in Approximation – Does this belong into NEWS?

Manuel Eberl eberlm at in.tum.de
Tue Jan 19 10:15:01 CET 2016

As of 67792e4a5486, I fixed a regression in the ‘approximation’ decision 
procedure that was introduced with Isabelle2015: approximating terms 
containing ‘powr’ did not work anymore due to the changed definition of 

It works again now and I was wondering whether this kind of thing should 
also be put into NEWS/CONTRIBUTORS.

(I have more changes to ‘approximation’ in my pipeline, but these are 
new features and performance improvements, which can wait until after 
the release, but I deemed it important to fix this regression after it 
already made it into the last release)


More information about the isabelle-dev mailing list