[isabelle] Isabelle2019-RC2 enat regression



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.

Cheers,
Gerwin


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