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

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;

more explicit discrimination of empty nodes -- suppress from Theories panel;

tuned;

tuned comments;

clarified module name: facilitate alternative GUI frameworks;

proper change of perspective for removed nodes (stemming from closed buffers);

tuned signature;

some robustification of console output;

updated ErrorList.jar;

discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;

evade problems with MikTeX on Windows;

tuned messages;

support multiple selected print operations instead of slightly odd "menu";

more default imports;

no keyword completion within word context -- especially avoid its odd visual rendering;

merged

merged

add parametricity lemmas

add lemma