Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -300 -100 -60 +60 +100 +300 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
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
(0) -1000 -300 -100 -60 +60 +100 +300 tip
nominal2