2015-05-04 wenzelm 2015-05-04 tuned;
2015-05-04 kuncar 2015-05-04 CONTRIBUTORS
2015-05-04 kuncar 2015-05-04 update isar-ref on Lifting
2015-05-04 kuncar 2015-05-04 NEWS
2015-05-04 wenzelm 2015-05-04 tuned;
2015-05-04 wenzelm 2015-05-04 more on GTK;
2015-05-04 wenzelm 2015-05-04 more on Isabelle document preparation and bibtex files;
2015-05-04 wenzelm 2015-05-04 tuned spelling;
2015-05-03 wenzelm 2015-05-03 updated screenshot;
2015-05-03 blanchet 2015-05-03 improved one-line preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
2015-05-03 blanchet 2015-05-03 made split-rule tactic go beyond constructors with 20 arguments
2015-05-03 wenzelm 2015-05-03 proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;
2015-05-03 wenzelm 2015-05-03 tuned output to resemble input syntax more closely;
2015-05-03 wenzelm 2015-05-03 updated Eisbach, using version fb741500f533 of its Bitbucket repository;
2015-05-03 wenzelm 2015-05-03 proper header;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-05-03 wenzelm 2015-05-03 tuned output;
2015-05-03 wenzelm 2015-05-03 tuned output -- avoid empty quites and extra breaks;
2015-05-03 wenzelm 2015-05-03 tuned;
2015-05-03 wenzelm 2015-05-03 suppress formal sort-constraints, in accordance to norm_hhf_eqs;
2015-05-03 wenzelm 2015-05-03 make SML/NJ more happy;
2015-05-03 wenzelm 2015-05-03 tuned message;
2015-05-02 kuncar 2015-05-02 add testing file for code_dt extension of lifting
2015-05-02 kuncar 2015-05-02 handle error messages also in after_qed
2015-05-02 kuncar 2015-05-02 reorder some steps in the construction to support mutual datatypes
2015-05-02 kuncar 2015-05-02 more readable error message if some types do not correspond to sort constraints of the datatype
2015-05-02 kuncar 2015-05-02 better precomputing
2015-05-02 kuncar 2015-05-02 equivalence in code_dt data structure must respect both rty and qty
2015-05-02 kuncar 2015-05-02 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
2015-04-13 kuncar 2015-04-13 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
2014-12-05 kuncar 2014-12-05 Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
2014-12-05 kuncar 2014-12-05 tuned proof; forget the transfer rule for size_fset
2014-12-05 kuncar 2014-12-05 return also which code equation was used; tuned
2014-12-05 kuncar 2014-12-05 publish lifting_forget and lifting_udpate interface
2014-12-05 kuncar 2014-12-05 note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
2014-11-18 kuncar 2014-11-18 export the result of lifting_def
2014-11-18 kuncar 2014-11-18 useful function
2014-11-18 kuncar 2014-11-18 parametrize liting of terms by quotients
2014-11-18 kuncar 2014-11-18 improve handling of predicators in rsp_thm
2014-11-18 kuncar 2014-11-18 tuned; store pred_simps
2014-11-18 kuncar 2014-11-18 lift_definition: return the result of lifting
2014-11-18 kuncar 2014-11-18 lift_definition: interface also with tactic
2014-11-18 kuncar 2014-11-18 generalize prove_schematic_quot_thm
2014-11-18 kuncar 2014-11-18 added pred_def, rel_eq_onp tuned
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-05-01 wenzelm 2015-05-01 tuned;
2015-05-01 wenzelm 2015-05-01 updated screenshot;
2015-05-01 wenzelm 2015-05-01 clarified markup range;
2015-05-01 wenzelm 2015-05-01 modifier markup for all parsed tokens; report literal token markup, before re-assignment;
2015-05-01 wenzelm 2015-05-01 updated screenshots;
2015-04-30 wenzelm 2015-04-30 updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
2015-04-30 wenzelm 2015-04-30 avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);
2015-04-28 blanchet 2015-04-28 allow sorts on dead variables in BNFs
2015-04-28 wenzelm 2015-04-28 tuned whitespace;
2015-04-28 wenzelm 2015-04-28 avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;
2015-04-27 wenzelm 2015-04-27 code equations as displayable content in code dependency graph
2015-04-27 wenzelm 2015-04-27 filtering of reflexive dependencies avoids problems with state-of-the-art graph browser; clarified
2015-04-25 wenzelm 2015-04-25 added checkbox for try0;