Script Management
Be careful with this, as it may delete more than you anticipate.
However, you can always recover the killed text using Emacs Undo.
Don't try this one at home, kids.
This is supplied in order
to enable the user to test the types and values of expressions. There's
some checking that the command won't change the proof state, but it
isn't foolproof.