On 03/01/2019 13:20, Chun Tian (binghe) wrote: > > I personally don’t like the keyword “Theorem” because I think many small > theorems with 3 lines of tactics do not deserve the name “Theorem”. The > correct way of using these conventions should be aligned with majority > math books, which I believe there must be some “rules” mentioned somewhere.
Isar started with 'theorem', then added 'lemma' and 'corollary', much
later 'proposition'.
In everyday use 'lemma' quickly became the most popular one. So if there
were only one keyword, it would be 'lemma'.
Makarius
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
