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;
2015-04-25 blanchet 2015-04-25 made CVC4 support work also without unsat cores
2015-04-24 wenzelm 2015-04-24 more paranoia settings, e.g. relevant for Ubuntu 15.04;
2015-04-24 wenzelm 2015-04-24 Added tag Isabelle2015-RC2 for changeset 8483c2883c8c
2015-04-24 wenzelm 2015-04-24 always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
2015-04-24 wenzelm 2015-04-24 tuned;
2015-04-24 wenzelm 2015-04-24 tuned message, in accordance to ML side;
2015-04-24 wenzelm 2015-04-24 tuned settings to avoid sporadic crashes;
2015-04-24 wenzelm 2015-04-24 clarified settings for default Poly/ML version: test the actual Isabelle component;
2015-04-22 blanchet 2015-04-22 avoid binding warning in Nitpick
2015-04-22 blanchet 2015-04-22 doc
2015-04-22 wenzelm 2015-04-22 clarified permissions;
2015-04-22 wenzelm 2015-04-22 allow diagnostic proof commands with skip_proofs;
2015-04-22 wenzelm 2015-04-22 tuned signature;
2015-04-22 wenzelm 2015-04-22 updated polyml according to fixes-5.5.2 SVN version 2009;
2015-04-20 blanchet 2015-04-20 declare Nitpick atoms to avoid '??.' prefixes in output
2015-04-19 wenzelm 2015-04-19 proper isatest machine;
2015-05-23 wenzelm 2015-05-23 prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
2015-05-12 nipkow 2015-05-12 this warning is hardly useful but produces noisy markers in the jedit interface
2015-05-09 nipkow 2015-05-09 undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
2015-05-07 hoelzl 2015-05-07 generalized tends over powr; added DERIV rule for powr
2015-05-06 blanchet 2015-05-06 added acknowledgment
2015-05-05 immler 2015-05-05 general Taylor series expansion with integral remainder