Remove TABs from examples

Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Overdue modernization of these examples.

Change to the inductive relations definition code to support a global, and
updated "monoset", which can be updated as theories load, thereby invisibly
increasing the capabilities of Hol_reln. Also simplify the implementation
of derive_strong_induction, and move the entrypoint to IndDefLib. New
test in src/IndDef/selftest.sml wouldn't have passed before (I believe).
It is more onerous than Peter's original monoset example, which didn't
feature recursion under the EVERY operator. Documented in Description and
release notes. Still to update theories with appropriate calls to
export_mono. (export_mono and export_rewrites are now part of bossLib's
interface.)

Move ind_def examples file (which now build, thanks Peter!) to
examples/ind_def so that we have one copy of these examples not two.
The directory src/IndDef/examples goes away. The clScript from the src
directory doesn't go over, because the one in examples has evolved a fair
bit (and now lies behind the Tutorial chapter).

These ancient examples have now been upgraded to work in Kananaskis.
Some of the proofs have been replaced by ones using modern tools, like
PROVE_TAC.

Started to modify in order to make this build under Kananaskis-0.
Didn't get any further than replacing basicHol90Lib with boolLib.

Changes to accomodate parser upgrade.

Initial revision