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);

more official Thy_Info.script_thy;

more frugal edits;

enable hires explictly, as seen for other high-end Java applications on the Web;

more markup;

another attempt at more aggressive auto-loading (amending af28fdd50690) -- hidden buffers are now suppressed;

more frugal edits;

more explicit treatment of cleared nodes (removal is implicit);

clarified display;

more workarounds for scalac;

clarified display;

avoid redundant data structure;