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.
 
2010-09-27 Christian Urban added simp rules for prod_fv and prod_alpha changeset | files
2010-09-26 Christian Urban a few more words about Ott changeset | files
2010-09-25 Christian Urban lifted size_thms and exported them as <name>.size changeset | files
2010-09-25 Christian Urban cleaned up two examples changeset | files
2010-09-25 Christian Urban added example about datatypes changeset | files
2010-09-23 Christian Urban updated to Isabelle 22 Sept changeset | files
2010-09-22 Christian Urban removed dead code changeset | files
2010-09-22 Christian Urban fixed changeset | files
2010-09-22 Christian Urban made supp proofs more robust by not using the standard induction; renamed some example files changeset | files
2010-09-20 Christian Urban introduced a general procedure for structural inductions; simplified reflexivity proof changeset | files
2010-09-17 Christian Urban updated to Isabelle Sept 16 changeset | files
2010-09-17 Christian Urban updated to Isabelle Sept 13 changeset | files
2010-09-12 Christian Urban tuned code changeset | files
2010-09-10 Christian Urban tuned (to conform with indentation policy of Markus) changeset | files
2010-09-10 Christian Urban supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance) changeset | files
2010-09-04 Christian Urban generated inducts rule by Project_Rule.projections changeset | files
2010-09-04 Christian Urban added the definition supp_rel (support w.r.t. a relation) changeset | files
2010-09-04 Christian Urban merged changeset | files
2010-09-03 Christian Urban got rid of Nominal2_Supp (is now in Nomina2_Base) changeset | files
2010-09-03 Christian Urban moved everything out of Nominal_Supp changeset | files
2010-09-03 Christian Urban renamed alpha_gen -> alpha_set and Abs -> Abs_set etc changeset | files
2010-09-03 Christian Urban moved a proof to Abs changeset | files
2010-09-03 Christian Urban got rid of Nominal_Atoms (folded into Nominal2_Base) changeset | files
2010-09-03 Christian Urban cleaned a bit various thy-files in Nominal-General changeset | files
2010-09-03 Christian Urban adapted paper to changes changeset | files
2010-09-03 Christian Urban made the fv-definition aggree more with alpha (needed in the support proofs) changeset | files
2010-09-03 Christian Urban removed lemma finite_set (already in simpset) changeset | files
2010-09-03 Christian Urban added supp_set lemma changeset | files
2010-09-02 Christian Urban some experiments with support changeset | files
2010-09-01 Christian Urban added eqvt-attribute for permute_abs lemmas changeset | files
2010-08-31 Christian Urban slides of my talk changeset | files
2010-08-30 Cezary Kaliszyk merge changeset | files
2010-08-30 Cezary Kaliszyk update qpaper to new isabelle changeset | files
2010-08-30 Cezary Kaliszyk No need to unfold mem_def with rsp/prs (requires new isabelle). changeset | files
2010-08-30 Cezary Kaliszyk Anonymize, change Quotient to Quot and fix indentation changeset | files
2010-08-29 Christian Urban renamed NewParser to Nominal2 changeset | files
2010-08-29 Christian Urban tuned changeset | files
2010-08-29 Christian Urban updated todos changeset | files
2010-08-28 Christian Urban added fs-instance proofs changeset | files
2010-08-28 Christian Urban added proofs for fsupp properties changeset | files
2010-08-28 Christian Urban fiexed problem with constructors that have no arguments changeset | files
2010-08-28 Christian Urban proved supports lemmas changeset | files
2010-08-28 Christian Urban slight cleaning changeset | files
2010-08-28 Christian Urban updated to new Isabelle changeset | files
2010-08-27 Christian Urban cut out most of the lifting section and cleaned up everything changeset | files
2010-08-27 Christian Urban made all typographic changes changeset | files
2010-08-27 Christian Urban first pass on section 1 changeset | files
2010-08-27 Christian Urban make copies of the "old" files changeset | files
2010-08-27 Cezary Kaliszyk Ball Bex can be lifted after unfolding. changeset | files
2010-08-26 Christian Urban "isabelle make test" makes all major examples....they work up to supp theorems (excluding) changeset | files
2010-08-26 Christian Urban merged changeset | files
2010-08-26 Christian Urban corrected bug with fv-function generation (that was the problem with recursive binders) changeset | files
2010-08-26 Cezary Kaliszyk minor changeset | files
2010-08-25 Christian Urban cleaned up (almost completely) the examples changeset | files
2010-08-25 Christian Urban cleaning of unused files and code changeset | files
2010-08-25 Christian Urban automatic lifting changeset | files
2010-08-25 Christian Urban everything now lifts as expected changeset | files
2010-08-25 Christian Urban now every lemma lifts (even with type variables) changeset | files
2010-08-25 Christian Urban can now deal with type variables in nominal datatype definitions changeset | files
2010-08-22 Christian Urban updated to new Isabelle changeset | files
2010-08-22 Christian Urban merged changeset | files
2010-08-22 Christian Urban updated to new Isabelle changeset | files
2010-08-21 Christian Urban not needed anymore changeset | files
2010-08-21 Christian Urban moved lifting code from Lift.thy to nominal_dt_quot.ML changeset | files
2010-08-21 Christian Urban nominal_datatypes with type variables do not work changeset | files
2010-08-21 Christian Urban changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default changeset | files
2010-08-20 Cezary Kaliszyk Clarifications to FIXMEs. changeset | files
2010-08-20 Cezary Kaliszyk Finished adding remarks from the reviewers. changeset | files
2010-08-20 Cezary Kaliszyk few remaining remarks as fixme's. changeset | files
2010-08-19 Christian Urban used @{const_name} hopefully everywhere changeset | files
2010-08-19 Cezary Kaliszyk Intuition behind REL changeset | files
2010-08-19 Cezary Kaliszyk add missing mathpartir changeset | files
2010-08-19 Cezary Kaliszyk Add 2 FIXMEs changeset | files
2010-08-19 Cezary Kaliszyk The type does determine respectfulness, the constant without an instantiated type does not. changeset | files
2010-08-19 Cezary Kaliszyk Add the SAC stylesheet and updated root file. changeset | files
2010-08-19 Cezary Kaliszyk TODO changeset | files
2010-08-19 Cezary Kaliszyk further comments from the referees changeset | files
2010-08-19 Cezary Kaliszyk fixes for referees changeset | files
2010-08-17 Christian Urban put everything in a "timeit" changeset | files
2010-08-17 Christian Urban improved runtime slightly, by constructing an explicit size measure for the function definitions changeset | files
2010-08-17 Christian Urban more tuning of the code changeset | files
2010-08-17 Christian Urban deleted unused code changeset | files
2010-08-17 Christian Urban improved code changeset | files
2010-08-16 Christian Urban can also lift the various eqvt lemmas for bn, fv, fv_bn and size changeset | files
2010-08-16 Christian Urban also able to lift the bn_defs changeset | files
2010-08-16 Christian Urban added rsp-lemmas for alpha_bns changeset | files
2010-08-16 Christian Urban cezary made the eq_iff lemmas to lift (still needs some infrastructure in quotient) changeset | files
2010-08-16 Christian Urban pinpointed the problem changeset | files
2010-08-16 Christian Urban modified the code for class instantiations (with help from Florian) changeset | files
2010-08-15 Christian Urban defined qperms and qsizes changeset | files
2010-08-15 Christian Urban simplified code changeset | files
2010-08-14 Christian Urban improved code changeset | files
2010-08-14 Christian Urban more experiments with lifting changeset | files
2010-08-12 Christian Urban updated to Isabelle 12th Aug changeset | files
2010-08-11 Christian Urban rsp for constructors changeset | files
2010-08-11 Christian Urban updated to Isabelle 11 Aug changeset | files
(0) -1000 -300 -100 -96 +96 +100 +300 tip
nominal2