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;

prevent beta-contraction in proving extra assumptions for abs_eq

more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);

reconfirm continuous checking on startup, to address common trap of disabling it accidentally;

tuned;

less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;

updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);

stick to external proofs when invoking E, because they are more detailed and do not merge steps

more robust handling of types for skolems (modeled as Frees)

tuning

repaired named derivations

use the noted theorems in 'BNF_Comp'

use the noted theorem whenever possible, also in 'BNF_Def'

use termtab instead of (perhaps overly sensitive) thmtab

use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)

tuned message;

added action "isabelle.options" (despite problems with initial window size);