[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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and