Quantifier improvements + invariant preservation in program transforms

update to libisabelle 0.3

print verification report after Isabelle phase

Added integration/evaluators/AbstractEvaluatorSuite.scala

5f9356bf broke this, but I can't blame @manoskouk, the code was indeed
messy.

(b) Fixing bugs in the benchmarks
(c) Makinging transformation phases of Orb ignore parts of the library

 * Expression grammars are now alwayse 'Labels -> Expr', simple grammars
   that are 'Type -> Expr' can simply extend SimpleExpressionGrammars

 * Labels now have Aspects. A label aspect describes a particular
   feature of the label (e.g. its size), as well as how this aspect
   applies to sub-productions.

   Aspects describe how sub-productions are generated/filtered/modified.
   See comments in Aspect for more information

Notable changes:
* sbt-libisabelle plugin which takes care of Isabelle source management
  - no more submodules; Isabelle sources are now packaged in JAR files
  - no weird ROOTS file in the repository root
* less isabelle: flags, everybody would want to use the defaults anyway
* updating to Isabelle2016 becomes possible (future work)