Make this more concise and clear by just presenting the lexical and syntactic
grammar as the way we define the Leo syntax, as opposed to discussing
alternatives like PEGs.
Explicate references to RFCs a bit.
Use the term 'sequence of terminals' instead of 'string' to avoid any confusion.
(Still use 'string' to refer to the actual strings in double quotes that are
part of the ABNF notation itself.)
Update to say that grammar is no longer just a draft.
Put primary motivation and purpose of grammar first.
Mention use in formalization second, and slightly simplify that part, given that
the formalization is not public yet.
This was uncovered by running the grammar through the ACL2 build: among other
things, the build checks that every nonterminal referenced in the right side of
each rule has a definition in the grammar.
