This suggestion was mine. Although “proposition” can mean many things, we are
talking about mathematical developments. Quite a common convention is to
reserve “theorem” for one or two main results, and “lemma” for technical
results of no general interest, leaving “proposition” as the main
On 07/10/2015 00:37, Michael Norrish wrote:
HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax fixities. I
don't think HOL Light supports comments at this level. HOL4 does, using SML's (* ... *).
So, if you want to write the escaped *, you have to use our older
