Fix examples/euclid.sml and make sure it's regression-tested

Errors caused by change to tight equality.

Euclid Tutorial chapter revisions almost complete

Make euclid.sml script idempotent.

Remove merge cruft (that should have been resolved before checkin) from r8378.

Synching remote copy. Also, fix to miller build
failure (NORM_TAC is more effective than before,
breaking the proof).

Fix Euclid example so that it works again.

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!

This check-in mainly fixes a problem with
literals occurring in patterns of TFL-style
definitions. There are a host of other minor
changes as well.

Fixed some broken proofs, and added some
new alternative proofs. Among other things,
moved to METIS_TAC from PROVE_TAC.

Mark Staples pointed out that autopilot didn't compile. I checked the
other easy examples in this directory, and found that two others
failed while proving things. In both cases, it was due to extra
normalisation done by arith_ss. So, mea culpa.

Adding in Peter Homeier's Sunrise system. None of the examples run yet,
since they depend on HOL strings being represented as constants,
which they are no longer.

However, the theories all build, and provide a major testcase for HOL.

Upgrading examples to match new stuff in system. The ind_def examples
are not yet fully integrated!

Tracking change of type of DECIDE.

Minor changes.

These examples now build in Kan.0.

Minor upgrades.

Updates to handle change to type of Q.prove.

Minor syntactic changes.

Removed the use of time in the call to load bossLib; it detracts from
the novice level of the example (see Tutorial chapter 4).

Fixed to bring it up to date with Taupo release 0.
(It used Infix as a fixity.)

Initial revision