note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional

export the result of lifting_def

useful function

parametrize liting of terms by quotients

improve handling of predicators in rsp_thm

tuned; store pred_simps

lift_definition: return the result of lifting

lift_definition: interface also with tactic

generalize prove_schematic_quot_thm

added pred_def, rel_eq_onp tuned

misc tuning, based on warnings by IntelliJ IDEA;

tuned;

updated screenshot;

clarified markup range;

modifier markup for all parsed tokens; report literal token markup, before re-assignment;

updated screenshots;

updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;

avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);

allow sorts on dead variables in BNFs

tuned whitespace;

avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;

code equations as displayable content in code dependency graph

filtering of reflexive dependencies avoids problems with state-of-the-art graph browser; clarified

added checkbox for try0;

made CVC4 support work also without unsat cores

more paranoia settings, e.g. relevant for Ubuntu 15.04;

Added tag Isabelle2015-RC2 for changeset 8483c2883c8c

always traverse required nodes, e.g. relevant for inlined errors of imported theory header;

tuned;

tuned message, in accordance to ML side;