Re: [isabelle] attribute "termination_simp" not documented?
> as far as I can tell the official Isabelle documentation does not
> mention the "termination_simp" attribute/named-theorem-collection. I
> would have expected to find it at least in "isabelle doc functions".
Thanks, this should definitely be mentioned. I just added it to the
function tutorial and the Isar reference manual for future reference.
This is after the Isabelle 2019 release train, but I guess that is fine.
This archive was generated by a fusion of
Pipermail (Mailman edition) and