Make various style tweaks, mostly to get line lengths <= 80 cols

Fix more definitions of ERR (examples/separationLogic)

Fix Holfoot pretty-printing

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.

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

Update of the interactive proof-scripts to make them better usable for the web-interface. Now some unimportant output is discarded and (more importantly) examples that are intended to fail are put into commented out.

The binary of the new command-line tool that is able to replay interactive proofs is huge (ca. 145 MB). So, now two version are build: a simple version (ca. 23 MB) and this full version.

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.

added a binary-search example that shows the usefulness of Yices

some more work on arrays, especially modifying predicate simpsets

some optimisations for arrays / support for HolSmtLib added

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

- make holfoot work again after the changes to the simplifier (arithmetic decision procedure)
- a lot of cleaning up of problems found by sanity-checks
- introduction of var_res_bigstar as a first step towards adding arrays

getting holfoot working with mosml