Faster PERM conv, add conv for ALL_DISTINCT.

Improves the performance of PERM_ELIM_DUPLICATES_CONV from O(n^2)
to O(nlogn) for large lists with many duplicates. This is done by
adding another phase that splits large problems with binary splits.

Also, add necessary helper lemmas about PERM to sortingTheory.

Adds a new conv ALL_DISTINCT_CONV which proves ALL_DISTINCT goals
by permuting to a strictly ordered list.

Remove TABs from src

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

cleanup of quantifier heuristics library

- more sensible names for guesses
- quantHeuristicsLib renamed to quantHeuristicsLibBase
- quantHeuristicsLibArgs renamed to quantHeuristicsLibParameters
- new shorter signature defined in quantHeuristicsLib
- adaptation of usage of quantHeuristicsLib

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

Remove trailing whitespace in source files.

Simplification for permutations that contain DROP and TAKE added.

PERM_SIMPLE_ss added.

The recently improved PERM_ss simplifies all permutations in its context. Often this is very benefitial. However, it avoids replacing a list with a larger list in a permutation. PERM_SIMPLE_ss does not simplifiy the permutations in its context. This allows simplifications like

(PERM small large ==> PERM (l1 ++ small) l2) <=>
(PERM small large ==> PERM (l1 ++ large) l2

Improvement of PERM_ss. Now the context is preprocessed instead of being used as it is.
This preprocessing allows problems like

``(PERM l1 m1 /\ PERM l2 m2 /\
PERM (l1 ++ l2) n1 /\ PERM (m1 ++ m2) n2) ==>
PERM n1 n2``

to be solved automatically. It is made available for assumptions as
NORMALISE_ASM_PERM_TAC.

removed some garbage in the code

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!

sortingTheory was extended by theorems about PERM. Most noteworthy might be the introduction of the relation PERM_SINGLE_SWAP relation and the proof that
PERM = TC PERM_SINGLE_SWAP holds. This allows to lift the theorems about transitive closures to PERM. Moreover, there are a lot of new theorems used by the new library permLib.

permLib contains tools for permutations. These tools are able to simplify permutations:

PERM_NORMALISE_CONV ``PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4)``

|- PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4) <=>
PERM (z::l4) (x::l1)

Moreover, there is support for replacing parts of lists with permutations

PERM_REWR_CONV (ASSUME ``PERM l1 [x;y;z]``) ``PERM (z::y::x'::l2) (l3++x'::l1)``

[PERM l1 [x; y; z]]
|- PERM (z::y::x'::l2) (l3 ++ x'::l1) <=> PERM (x::l3) l2 : thm

These and other conversions have been added to a simpfrag called PERM_ss.