Remove TABs from examples

Remove eqtype declaration for term type

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.

rename most occurences of the prefix "FASL" into "ASL"

The prefix ASL (Abstract Separation Logic) was used to indicate definitions related to Abstract Separation Logic. To distinguish definitions that were not aware of the special failiure state (like asl_star) and ones that were (fasl_star) the additional prefix FASL (Abstract Separation Logic with Failiure State) was used as well. However, in the end, most definitions had the FASL prefix which does not make much sense. So, the prefix was replaced by ASL expect for cases where it is really important to distinguish between versions of a definition that are aware of the failiure state and ones that are not.

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

some minor fixes and extensions:
- parser allows call-by-value arguments in HOL-expressions now
- fixing pretty printing problem of call-by-reference arguments in abstracted function calls
- some minor changes in the order of inference applications

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

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!

A case study that reimplements parts of smallfoot inside HOL

Initial revision of a framework for separation logic, that is based on abstract separation logic. Currently it contains a formalisation of abstract separation logic and some theorems about read/write permissions for stack variables.