fixed then-else confusion

tweak Vampire setup in the light of new evaluation

improved set of reconstructor methods

warn users about unused "using" facts

be less aggressive at kicking out chained facts

recognize bus errors as crash

consider removing chained facts last, so that they're more likely to be kept

clarified format of etc/options: only declarations, not re-definitions;

check_errors for cumulative session content;

even more defensive path expansion (see also 8d381fdef898);

support for 'typ' with explicit sort constraint;

added jedit option -d;

always retain doc-src (as regular component);

merged

Calling isabelle with proper (relative) path, no longer relying on $PATH.

fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;

updated to jedit-4.5.2 (still unchanged);

restored ISABELLE_OUTPUT etc -- still relevant at least for mira.py itself

tuned;

fixed mira.py (cf. fd50596bf78b)

more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;

more static antiquotations;

always show some timing information, to reduce the need for explicit -v;

some information for central Isabelle repository configuration;

reduced settings patching

removed obsolete configuration AFP_images

faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;

simplified symbol matching;

further clarification of malformed symbols;

more liberal scanning of potentially malformed symbols;