Re: [isabelle] Isabelle2019-RC2 enat regression

Ah yes, this change set was after the Isabelle2019-RC2 fork point.

Sorry for the noise, then. It’s not a regression, it’s something that hadn’t worked before and now does work in isabelle devel, but not RC2. Nothing that needs to be done.


On 19 May 2019, at 14:50, Denis Nikiforov <denis.nikif at<mailto:denis.nikif at>> wrote:


Such expressions began to be simplified after this change:
So I updated a proof to let the AFP entry build successfully:
Maybe this change was reverted in the latest revision...

вс, 19 мая 2019 г. в 04:31, Klein, Gerwin (Data61, Kensington NSW) <Gerwin.Klein at<mailto:Gerwin.Klein at>>:
While updating an AFP entry I found what seems to be a regression for the type enat in Isabelle2019-RC2:

“1 <= (20::enat)” seems to have normalised by simp automatically, but does not any more.

Something like (simp flip: enat_numeral add: one_enat_def) does it, but is not very nice.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.