Remove trailing whitespace.

Fix a bug with respect to handling resources and conditional critical regions. Additional features like nodetermistic-choice, diverge and fail statements lifted to the user-level.

support for global specification variables added to the parser

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.

Update of the parser to allow the new keyword "old" to refer to the old values of variables, i.e. the values in the precondition. At the same time the interaction between HOL's and Holfoot's parser was improved. Now Holfoot-variables are better replaced in HOL-terms (i.e. Holfoot knows about lambda-abstraction now).

- assertions added
- loop unrolling added
- parser improved
- more examples (fact.dsf / append-unroll.dsf)

Main goal: improve usability of loop-specifications

Added a way to parse arbitray Holfoot predicates using h``complicated pred``. In contrast ``xxx`` works just for xxx that are of type bool. An example has been added in entailments.ent

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

- 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.

improvements to the parser (better error reporting, more arithmetic operations) as well as
addition of loop- and block-specifications with corresponding examples

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