compile

more robustness in Isar proof construction

tuning

merged

more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;

tuned code

having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations

store explicitly quotient types with no_code => more precise registration of code equations

don't needlessly regenerate entire file when the time stamps are equal

eliminated source of 'DUP's in MaSh

fixed sorting (broken since 9cc802a8ab06)

reenabled MaSh for Isabelle2014 release (hopefully)

beware of duplicate fact names

refined filter for ATP steps to avoid 'have True' steps in E proofs

filter out 'theory(...)' from dependencies early on

introduce fact chaining also under first step

'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)

merged

proper perl;

less warnings -- ignore potential prover startup/shutdown races;

tuned spelling;

further distinction of Isabelle distribution: alert for identified release candidates;

updated to scala-2.11.2;

clarified file names;

less ambitious isatest, avoid "Exception- InternalError: Backing up too far (32bit) raised while compiling" in polyml-5.4.1;

tuned imports;

proper scope of comments;

make SML/NJ happy;