handle Vampire's definitions smoothly

fix bug in direct Isar proofs, which was exhibited by the "BigO" example

honor "xsymbols"

kill another neg_clausify proof

show types in Isar proofs, but not for free variables; this makes proofs more robust, without as much clutter as there used to be when types were enabled previously

give more helpful error message

first proposal for a announcement

NEWS (more strict internal axioms/defs format)

one all-inclusive bundle for each platform;

more robust handling of additional type variables: warning, more canonical order, drop mixfix syntax if implicit type arguments are introduced (to avoid delusion due to shifted arguments);

tuned warning;

less ambitious settings;