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 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip

tuned output;
2015-05-03, by wenzelm
tuned output;
2015-05-03, by wenzelm
tuned output;
2015-05-03, by wenzelm
tuned output;
2015-05-03, by wenzelm
tuned output -- avoid empty quites and extra breaks;
2015-05-03, by wenzelm
tuned;
2015-05-03, by wenzelm
suppress formal sort-constraints, in accordance to norm_hhf_eqs;
2015-05-03, by wenzelm
make SML/NJ more happy;
2015-05-03, by wenzelm
tuned message;
2015-05-03, by wenzelm
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

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

isabelle