Re: [isabelle] attribute "termination_simp" not documented?



Hi Chris,

> 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.

Alex




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