made split-rule tactic go beyond constructors with 20 arguments

proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;

tuned output to resemble input syntax more closely;

updated Eisbach, using version fb741500f533 of its Bitbucket repository;

proper header;

tuned output;

tuned output;

tuned output;

tuned output;

tuned output -- avoid empty quites and extra breaks;

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