[isabelle] datatype_compat in Isabelle2018-RC0



The datatype_compat command used to generate the old-style definition of the “size” constant in Isabelle2017 (potentially only when  size did not yet exist). This no longer seems to be the case.

Is this intentional? I couldn’t find anything relevant in NEWS.

I’m using this a few times — not very often, but it’s annoying enough to recreate manually (see email thread on that around Isabelle2017..) that it’s worth checking at least.

Cheers,
Gerwin



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