Remove TABs from source files (and some trailing w/space)

Added self tests

Fixed modelCheckLib with NuSMV model checker

Fixed use of the old syntax for conditional expressions in temporalLib

Fixed src/temporal/examples.sml with HOL4_SMV_EXECUTABLE=NuSMV

Remove TABs from src

Will also make selftest to check that they aren't introduced

Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Clean src/ to remove Unicode (or to mark it as OK)

Marking Unicode as OK is done by putting the UOK tag on the same line of
the relevant file.

double 'the' removed

temporalLib was failing to load. ratLib was referring to the defunct ``ALT_ZERO``. Also make permLib load without inventing a type variable.

Fix a couple of Latin-1 comments so that they're now UTF-8

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!

Some fixes needed to get HOL to build. (Brought on by supporting the Standard ML Basis Library).

Added a new function SMV_RUN_FILE that allows to pass an arbitrary program to SMV. While SMV_RUN accepts this programm as a string, SMV_RUN_FILE expects a filename and runs SMV on the specified file. Internally SMV_RUN uses SMV_RUN_FILE.

Added a new function SMV_RUN that allows to pass an arbitrary program to SMV.

Fixed some bugs, occuring because of a changed behavior of CHANGED_CONV

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

src/temporal now builds in Kan. 0.

Removed dependency on global grammar, which was causing grief when
loading in a context where integers were around.

Minor changes.

New library for temporal logic, from Klaus Schneider.