holfoot example: add selftests

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.

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.

- fix of the recently broken quicksort-proof-script
- parser detects duplicate function and resource definitions now
- added debugging options to the command line tool

fix problems with mosml-version

extensions of the interface / easier addition of own tactics

- 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

Added an option to the command-line tool to run interactive proof scripts. The proof scripts have been updated to work with this new feature.

some more work on arrays, especially modifying predicate simpsets

some more support for arrays and a new q uicksort example using arrays

some minor improvements on the command line tool and the holfoot

A lot of minor changes:
- introduction of gen_step_tac_opt, i.e. new interface to most holfoot tactics
- stopping simulation at specific points like loops, abstractions etc. added
- renaming of holfoot tactics
- better support for LAST and FIRST in specifications
- holfoot_interactive_verify_spec and similar functions improved
- holfoot_set_goal_preprocess and holfoot_set_goal_procedures added

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