Mods to get examples working again.

Changed behaviour of simplifier to
propagate the abbreviation coming from
a let binding in the goal being moved to
the assumptions. This helps keep the goal
in "fully abbreviated form". Also added

Q.REABBREV_TAC

which re-abbreviates the goal and

Q.WITHOUT_ABBREVS tac

which temporarily removes all abbreviations,
runs tac, then reabbreviates.

Probably, Q is not the right place for these
functions, but the rest of the abbreviation
stuff is there.

Also added some internal documentation on what
Q.ABBRS_THEN does, and the like.

Revised example so that it works and is simpler.

Minor changes.

Final fixes to separate schematic definitions from ordinary ones.
Also, some of the examples have been polished a bit.

Minor editing.

New examples (well, tarted up old ones) showing how nested rec.
functions can be proved to terminate.