header tuning

correctly translate THF functions from terms to types

do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly

back to post-release mode -- after fork point;

tuned;

tuned;

no -optimise -- produces bad bytecode;

output state first -- avoid fluctuation wrt. warnings, errors, etc.;

tuned comment;

updated to polyml-5.5.2-1 which addresses two hard crashes;

updated to cygwin-20140725, which is presumably close to Cygwin 1.7.31-1;

added more functions and lemmas

proper mkdir;

proper option -O;

some reshuffling of Poly/ML version to evade failing tests;

old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;

proper volume name, such that background image is found in /Volumes/Isabelle/.background;

tuned;

tuned message;

setup for drag-and-drop DMG;

merge

reordered provers

compile

faster minimization by not adding facts that are already in the simpset

added missing facts to proof method

don't lose 'minimize' flag before it reaches Isar proof text generation

tuning

avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)

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;