Fix more definitions of ERR (examples/separationLogic)

Holfoot example: repair bit rot

Delete trailing whitespace

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

Remove trailing whitespace in source files.

Examples from VSTTE-competition added. For example vscomp4 the parser was modified to support user defined predicates. As part of this change the syntax for trees changed.

- add multiple levels for expansions by holfoot-tactics, there were no_expands and do_expands, now there is full_expands as well. full_expands behaves like the old do_expands. do_expands does just fast expansions now
- fix a bug in the handling of assertions
- example array-inc added
- example quicksort-full-loopspec added

Adding examples binary-search and array-copy that use loop-specs instead of loop-invariants. Some minor cleanups in the thories for the sake of better readablity and documentation.

some more work on arrays, especially modifying predicate simpsets

- adaption to the recent changes to listTheory / listSimps / rich_listTheory.
- some support for arrays added

Mayor refactoring of the Holfoot-Parser. The parser now uses the abstract syntax of HOL internally, which allows it to pass typing information between different parts of the input much more efficiently. As a result, most type-annotations could be removed from the input files. Moreover, it's now possible to write HOL terms as expressions inside a program now. These expressions have to return a value of type num and may take program variables as input. For example programs like "x = ``MAX y z``" can be written now, where "x", "y" and "z" are variables of the programming language. A similar extension has been added for conditions of loops and if-then-else statements. Finally, there is a predicate for separating mapping and predicate for queues now.

A lot of minor tweaks and additions. The main ones are:

- parser can handle trees better now
- better support for call-by-value arguments by the parser
- inference for splitting of non-empty trees added
- option to turn of expanding specifications added to main tactics
- NUM_TO_BOOL added
- slightly extended treeTheory

This is a major refactoring of the separation-logic example. The main changes are:

- the smallfoot case study has been renamed to "holfoot"
- a lot of the results of the smallfoot case study were generalised to the "variables as resource" level of abstraction
- this generalisation allows much shorter and easier proofs for the remaining results
- new methods for handling conditional execution, while-loops and procedure calls implemented
- generalisation of the concept of ghost variables (e.g. limitation on the possible types of ghost variables removed)
- addition of comments that keep track of the current position in the program, thereby giving
useful feedback to the user during interactive proofs or when a proof-attempt fails
- rewritten automation in order to
- make extensions of the programming and specification language easier
- keep track of location comments
- increase speed
- pretty printing uses styles (i.e. colors, bold fonts, etc.) now
- tree predicate of smallfoot generalised to allow data in trees as well as arbitrary n-ary trees
- holfoot command line tool added