Allow commentes in more places (i.e. after Case)

This change breaks support for strings including --.
Add syntax for step annotations
syntax for named axioms, lemmas
Require steps to be annotated with lemma