isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

add testing file for code_dt extension of lifting
2015-05-02, by kuncar
handle error messages also in after_qed
2015-05-02, by kuncar
reorder some steps in the construction to support mutual datatypes
2015-05-02, by kuncar
more readable error message if some types do not correspond to sort constraints of the datatype
2015-05-02, by kuncar
better precomputing
2015-05-02, by kuncar
equivalence in code_dt data structure must respect both rty and qty
2015-05-02, by kuncar
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-05-02, by kuncar
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
2015-04-13, by kuncar
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
2014-12-05, by kuncar
tuned proof; forget the transfer rule for size_fset
2014-12-05, by kuncar
return also which code equation was used; tuned
2014-12-05, by kuncar
publish lifting_forget and lifting_udpate interface
2014-12-05, by kuncar
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
2014-12-05, by kuncar
export the result of lifting_def
2014-11-18, by kuncar
useful function
2014-11-18, by kuncar
parametrize liting of terms by quotients
2014-11-18, by kuncar
improve handling of predicators in rsp_thm
2014-11-18, by kuncar
tuned; store pred_simps
2014-11-18, by kuncar
lift_definition: return the result of lifting
2014-11-18, by kuncar
lift_definition: interface also with tactic
2014-11-18, by kuncar
generalize prove_schematic_quot_thm
2014-11-18, by kuncar
added pred_def, rel_eq_onp tuned
2014-11-18, by kuncar
misc tuning, based on warnings by IntelliJ IDEA;
2015-05-03, by wenzelm
tuned;
2015-05-01, by wenzelm
updated screenshot;
2015-05-01, by wenzelm
clarified markup range;
2015-05-01, by wenzelm
modifier markup for all parsed tokens;
2015-05-01, by wenzelm
updated screenshots;
2015-05-01, by wenzelm
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
2015-04-30, by wenzelm
avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);
2015-04-30, by wenzelm
allow sorts on dead variables in BNFs
2015-04-28, by blanchet
tuned whitespace;
2015-04-28, by wenzelm
avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;
2015-04-28, by wenzelm
code equations as displayable content in code dependency graph
2015-04-27, by wenzelm
filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
2015-04-27, by wenzelm
added checkbox for try0;
2015-04-25, by wenzelm
made CVC4 support work also without unsat cores
2015-04-25, by blanchet
more paranoia settings, e.g. relevant for Ubuntu 15.04;
2015-04-24, by wenzelm
Added tag Isabelle2015-RC2 for changeset 8483c2883c8c
2015-04-24, by wenzelm
always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
2015-04-24, by wenzelm
tuned;
2015-04-24, by wenzelm
tuned message, in accordance to ML side;
2015-04-24, by wenzelm
tuned settings to avoid sporadic crashes;
2015-04-24, by wenzelm
clarified settings for default Poly/ML version: test the actual Isabelle component;
2015-04-24, by wenzelm
avoid binding warning in Nitpick
2015-04-22, by blanchet
doc
2015-04-22, by blanchet
clarified permissions;
2015-04-22, by wenzelm
allow diagnostic proof commands with skip_proofs;
2015-04-22, by wenzelm
tuned signature;
2015-04-22, by wenzelm
updated polyml according to fixes-5.5.2 SVN version 2009;
2015-04-22, by wenzelm
declare Nitpick atoms to avoid '??.' prefixes in output
2015-04-20, by blanchet
proper isatest machine;
2015-04-19, by wenzelm
prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
2015-05-23, by wenzelm
this warning is hardly useful but produces noisy markers in the jedit interface
2015-05-12, by nipkow
undid 6d7b7a037e8d because it does not help but slows simplification down by up to 5% (AODV)
2015-05-09, by nipkow
generalized tends over powr; added DERIV rule for powr
2015-05-07, by hoelzl
added acknowledgment
2015-05-06, by blanchet
general Taylor series expansion with integral remainder
2015-05-05, by immler
generalized class constraints
2015-05-05, by immler
generalized differentiable_bound; some further variations of differentiable_bound
2015-05-05, by immler

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

isabelle