Remove TABs from examples

Remove trailing whitespace in source files.

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.

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.

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

Main goal: improve usability of loop-specifications

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

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