Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -300 -100 -96 +96 +100 +300 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
2011-05-09 Christian Urban merged changeset | files
2011-05-03 Christian Urban added two mutual recursive inductive definitions changeset | files
2011-05-03 Christian Urban deleted two functions from the API changeset | files
2011-05-03 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates) changeset | files
2011-05-09 Christian Urban more on pearl-paper changeset | files
2011-05-04 Christian Urban more on pearl-paper changeset | files
2011-05-02 Christian Urban updated Quotient paper so that it compiles again changeset | files
2011-04-28 Christian Urban merged changeset | files
2011-04-28 Christian Urban added slides for beijing changeset | files
2011-04-21 Christian Urban more to the pearl paper changeset | files
2011-04-19 Christian Urban updated to snapshot Isabelle 19 April changeset | files
2011-04-18 Christian Urban merged changeset | files
2011-04-18 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April changeset | files
2011-04-15 Cezary Kaliszyk New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs. changeset | files
2011-04-13 Christian Urban merged changeset | files
2011-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive changeset | files
2011-04-12 Christian Urban shanghai slides changeset | files
2011-04-11 Christian Urban pictures for slides changeset | files
2011-04-11 Christian Urban Shanghai slides changeset | files
2011-04-10 Christian Urban more paper changeset | files
2011-04-09 Christian Urban eqvt of supp and fresh is proved using equivariance infrastructure changeset | files
2011-04-09 Christian Urban more paper changeset | files
2011-04-09 Christian Urban more on the paper changeset | files
2011-04-08 Christian Urban tuned paper changeset | files
2011-04-08 Christian Urban tuned paper changeset | files
2011-04-08 Christian Urban typo changeset | files
2011-04-08 Christian Urban more on paper changeset | files
2011-04-07 Christian Urban eqvt_lambda without eta-expansion changeset | files
2011-04-06 Christian Urban changed default preprocessor that does not catch variables only occuring on the right changeset | files
2011-03-31 Christian Urban final version of slides changeset | files
2011-03-30 Christian Urban more on the slides changeset | files
2011-03-30 Christian Urban tuned IsaMakefile changeset | files
2011-03-29 Christian Urban rearranged directories and updated to new Isabelle changeset | files
2011-03-16 Christian Urban precise path to LaTeXsugar changeset | files
2011-03-16 Christian Urban a lit bit more on the pearl-jv paper changeset | files
2011-03-16 Christian Urban ported changes from function package....needs Isabelle 16 March or above changeset | files
2011-03-14 Christian Urban more on the pearl paper changeset | files
2011-03-14 Christian Urban equivariance for All and Ex can be proved in terms of their definition changeset | files
2011-03-11 Christian Urban more on the paper changeset | files
2011-03-08 Christian Urban merged changeset | files
2011-03-08 Christian Urban more on the pearl paper changeset | files
2011-03-02 Cezary Kaliszyk distinct names at toplevel changeset | files
2011-03-02 Cezary Kaliszyk merge changeset | files
2011-03-02 Cezary Kaliszyk Pairing function changeset | files
2011-03-02 Christian Urban updated pearl papers changeset | files
2011-03-01 Christian Urban a bit more tuning changeset | files
2011-02-28 Christian Urban included old test cases for perm_simp into ROOT.ML file changeset | files
2011-02-28 Christian Urban split the library into a basics file; merged Nominal_Eqvt into Nominal_Base changeset | files
2011-02-25 Christian Urban some slight polishing changeset | files
2011-02-24 Christian Urban merged changeset | files
2011-02-24 Christian Urban added a lemma about fresh_star and Abs changeset | files
2011-02-23 Cezary Kaliszyk Reduce the definition of trans to FCB; test that FCB can be proved with simp rules. changeset | files
2011-02-19 Cezary Kaliszyk typeschemes/subst changeset | files
2011-02-17 Cezary Kaliszyk further experiments with typeschemes subst changeset | files
2011-02-17 Cezary Kaliszyk Finished the proof of a function that invents fresh variable names. changeset | files
2011-02-16 Christian Urban added eqvt for length changeset | files
2011-02-16 Christian Urban added eqvt lemmas for filter and distinct changeset | files
2011-02-07 Christian Urban added eqvt for cartesian products changeset | files
2011-02-07 Christian Urban cleaned up the experiments so that the tests go through changeset | files
2011-02-04 Cezary Kaliszyk merge changeset | files
2011-02-04 Cezary Kaliszyk Experiments defining a function on Let changeset | files
2011-02-04 Christian Urban updated TODO changeset | files
2011-02-04 Christian Urban Lambda.thy which works with Nominal_Isabelle2011 changeset | files
2011-02-03 Christian Urban merged changeset | files
2011-02-03 Christian Urban removed diagnostic code changeset | files
2011-02-01 Cezary Kaliszyk Only one of the subgoals is needed changeset | files
2011-01-31 Cezary Kaliszyk Experiments with substitution on set+ changeset | files
2011-01-31 Cezary Kaliszyk More properties that relate abs_res and abs_set. Also abs_res with less binders. changeset | files
2011-01-30 Cezary Kaliszyk alpha_res implies alpha_set :) changeset | files
2011-01-30 Cezary Kaliszyk Showing that the binders difference is fresh for the left side solves the goal for 'set'. changeset | files
2011-01-29 Cezary Kaliszyk Experiments with functions changeset | files
2011-01-27 Christian Urban some experiments changeset | files
2011-01-27 Christian Urban the proofs with eqvt_at changeset | files
2011-01-25 Christian Urban made eqvt-proof explicit in the function definitions changeset | files
2011-01-24 Cezary Kaliszyk merge changeset | files
2011-01-24 Cezary Kaliszyk minor changeset | files
2011-01-24 Cezary Kaliszyk Down as infixr changeset | files
2011-01-23 Christian Urban added some slides changeset | files
2011-01-23 Christian Urban added Tutorial6 changeset | files
2011-01-23 Christian Urban cleaning up changeset | files
2011-01-22 Christian Urban merged changeset | files
2011-01-22 Christian Urban cleaned up Tutorial 3 with solutions changeset | files
2011-01-22 Cezary Kaliszyk Missing val.simps changeset | files
2011-01-22 Cezary Kaliszyk merge changeset | files
2011-01-22 Cezary Kaliszyk Tutorial 4s changeset | files
2011-01-22 Christian Urban cleaned up and solution section changeset | files
2011-01-22 Christian Urban cleaned up tutorial1...added solution file changeset | files
2011-01-22 Christian Urban better version of Tutorial 1 changeset | files
2011-01-21 Christian Urban better flow of proofs and definitions and proof changeset | files
2011-01-21 Christian Urban separated type preservation and progress into a separate file changeset | files
2011-01-21 Christian Urban substitution lemma in separate file changeset | files
2011-01-21 Christian Urban added unbind example changeset | files
2011-01-20 Christian Urban a bit tuning changeset | files
2011-01-20 Christian Urban first split of tutorrial theory changeset | files
2011-01-19 Christian Urban added a very rough version of the tutorial; all seems to work changeset | files
2011-01-19 Christian Urban added obtain_fresh lemma; tuned Lambda.thy changeset | files
(0) -1000 -300 -100 -96 +96 +100 +300 tip
nominal2