Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 22 2022 at 19:54):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,

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

cheers

chris

view this post on Zulip Email Gateway (Aug 22 2022 at 19:54):

From: Alexander Krauss <krauss@in.tum.de>
Hi Chris,

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

Last updated: Apr 25 2024 at 16:19 UTC