tuned;

suppress formal sort-constraints, in accordance to norm_hhf_eqs;

make SML/NJ more happy;

tuned message;

add testing file for code_dt extension of lifting

handle error messages also in after_qed

reorder some steps in the construction to support mutual datatypes

more readable error message if some types do not correspond to sort constraints of the datatype

better precomputing

equivalence in code_dt data structure must respect both rty and qty

don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned

go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used

Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype

tuned proof; forget the transfer rule for size_fset

return also which code equation was used; tuned

publish lifting_forget and lifting_udpate interface

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;

tuned settings to avoid sporadic crashes;

clarified settings for default Poly/ML version: test the actual Isabelle component;

avoid binding warning in Nitpick

doc

clarified permissions;

allow diagnostic proof commands with skip_proofs;

tuned signature;

updated polyml according to fixes-5.5.2 SVN version 2009;

declare Nitpick atoms to avoid '??.' prefixes in output

proper isatest machine;