Fix theorem-prover/lisp-runtime for new by

More theorem-prover fixes for pat_assum rename

Partial fix for issue #127.

The definition of "remove_parse_stack" now works for the "classic heuristic" (set using PmatchHeuristics) but still fails for the "default". For the time being, an argument could be making the "classic" the default again, since it appears to be more stable.

The pertinent change was in Defn.wfrec_eqns, where "elim_triv_literal_CONV" is now incorporated into "rule". Other changes are tidy-ups.

rearranging files in examples/machine-code to separate decompiler from ISA models

split lisp_symbols into separate files

A mechanised soundness proof for a reflective theorem prover.