Move stuff into HOL/examples (upgrade!); progress w/completeness.

The necessary HOL commit is 33ec65435c.
translator now produces lowercase function names (even for I, S and K etc.)
Prove more things not nullable
More nullable theorems.
Prove firstSet values for the various expression non-terminals.

Lots of cut-and-pasting of tactics. Could probably be done more
automatically.
More nullability results needed.
More completeness cases (42 still to go)
Merge branch 'master' into tup+eq
More printer testing