On 03/01/2019 11:23, Chun Tian (binghe) wrote: > Hi Michael, > > thanks for fixing the bugs. (now I see why I can’t find its definition…) > > Going in this direction, have you considered adding also “Lemma” and > “Corollary”? Internally they're equivalent with “Theorem”, but they could > literally help writers (and readers) identifying different levels of > theorems, like those in math books.
This reminds me of Isabelle/Isar. Some decades ago I introduced these
variants of 'theorem' and it became a running gag of confusion and
unclear corner cases, because aliases were not really identical, but
distinguished internally by some tools.
Recently, we even introduced 'proposition' as another variant, but it is
unclear if it is more prominent than 'theorem' or less prominent than
'lemma'. Thus it depends on local conventions of particular
formalization projects how to treat it, e.g. in document presentation.
If I had another chance today, I would probably eliminate all funny
aliases of Isar commands.
Makarius
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
