Stop emacs-mode causing an extra Raise when applying a tactic.

The e and expandf functions in the proof manager already do a Raise as
it is.
Tell the interactive session to treat PolyML as already loaded.
Some new theorems about derivation sequences for the parsing example