add manual pattern match heuristic / improve exhaustive one

Implement a new pattern match heuristic that allows manually
specifying in which order to do case splits. This one prints
a lot of debugging information in order to allow the user to
make decent choices. The techniques for producing this debug
have also been added to the exhaustive tactic. It now prints
debugging information on how far the exhaustive search
progressed and on intermediate results

cleanup of Pmatch

Following a suggestion of Anthony, I cleaned-up the interface of Pmatch.
To this end, I moved much of the heuristics-code to a new library called
PmatchHeuristics. This new library is used by Pmatch. This allows to
clean-up the code and interface of Pmatch. If less frequently used functions
are needed, the library PmatchHeuristics has to be used now.

added trace "pp_cases" that allows to turn pretty-printing for case-expressions off

added exhaustive pattern match heuristic (useful only for very small examples)

execute several heuristics for pattern-matching and choose the best result
interface of pattern matching simplified

implemented qba heurtic for pattern matching; don't do splits for which
lead to same result for all cases

started with writing more complex pattern match heuristics

modify pattern matching to use heuristics for picking the column to split on

Remove duplication of code between Pmatch and TypeBasePure.

The case-syntax code in the latter has moved entirely to Pmatch.

Changes bringing Pmatch more into line with revisions to tfl’s Functional.sml.

Move mk_pattern_fn from old Functional structure to Pmatch.

Change src/bool to src/1 as a prelude to experimentation!