Remove TABs from src

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

Add syntax/ops to make set manipulations easier

Fixed implementation of PFset_conv.MAX_SET_CONV

Thanks to Konrad for the fix. With some regression tests.

Fix PFset_conv to not quote terms in one of its internal proofs.

The problem with this is that later theories may overload "SIGMA" or
other constants, thereby changing the meaning of this code when it's
evaluated. (Indeed, this is exactly what code in src/probability did
do.) Good practice, thus, is not to use the parser in library code, or
to rebind the parser so that it is not using the global grammar.

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!

Getting rid of some pattern-matching complaints,
as Anthony suggested.

hanges to upgrade EVAL on BIGUNION {}.



M src/parse/term_grammar.sig
M src/pred_set/src/pred_setScript.sml
M src/pred_set/src/pred_setLib.sml
M src/pred_set/src/PFset_conv.sml

Added powerset operator and simple theorems (finiteness, cardinality).
EVAL has been taught about it, etc.

EVAL now works for set expressions. Almost the full language of
sets is accepted, e.g., equality between finite sets, membership,
set comprehension, union, intersection, difference, deletion,
image, cardinality, finiteness, etc. Generally, the actual sets
have to be finite enumerations. Occasionally, variables for
the elements may be used. Some of the underlying algorithms
are quadratic, so not everything will scale up.

Also, there's now a full pred_setSyntax.sml.

Fix for IMAGE_CONV (provided by Peter Homeier), and selftest examples
to help it not happen again.

Fixed Lockwood Morris' problem with UNION_CONV.

Fixed bug in set conversions: the constant IN is no longer defined in
pred_setTheory, but in boolTheory, for some reason.

Also added rudimentary syntax support for sets.

Now builds in Kan.0.

Kananaskis compatibility.

Minor typographical changes.

Attempt to parse (--`\/`--) failed, and needed to be replaced by
(--`$\/`--).

Initial revision