inconsistent spelling (capitalization): goal, Lemma

[jwaldmann]

• in theory texts, lower case: axiom, goal.
• in proof texts: upper case: Lemma, Proof, QED, IH
• ... and lower case: def

I find upper case very inconvenient for typing (needs one more key). Does it improve readability? Not sure. "QED" definitely feels overdone. (Or is this because Latin didn't have lower case letters at all?)

How does Isabelle do it - all keywords start with lowercase letter?

[larsrh]

Yes, keywords are all lowercase. Sometimes things get all caps identifiers, e.g. in Isabelle/ML code.

[larsrh]

We could switch to a lowercase convention in cyp too. I don't feel strongly about it.