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

Makarius makarius at sketis.net
Tue Jan 19 11:11:28 CET 2016


On Tue, 19 Jan 2016, Manuel Eberl wrote:

> 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 
> ‘powr’.
>
> It works again now and I was wondering whether this kind of thing should also 
> be put into NEWS/CONTRIBUTORS.

>From the size and significance of the changeset, I would say yes.


 	Makarius


More information about the isabelle-dev mailing list