Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -240 +240 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
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
2011-01-19 Christian Urban base file for the tutorial (contains definitions for heigt, subst and beta-reduction) changeset | files
2011-01-19 Christian Urban ported some of the old proofs to serve as testcases changeset | files
2011-01-19 Christian Urban added eqvt and supp lemma for removeAll (function from List.thy) changeset | files
2011-01-19 Christian Urban theory name as it should be changeset | files
2011-01-19 Christian Urban removed diagnostic code changeset | files
2011-01-19 Christian Urban added Minimal file to test things changeset | files
2011-01-19 Christian Urban defined height as a function that returns an integer changeset | files
2011-01-18 Christian Urban deleted diagnostic code changeset | files
2011-01-18 Christian Urban some tryes about substitution over type-schemes changeset | files
2011-01-18 Christian Urban defined properly substitution changeset | files
2011-01-18 Christian Urban derived stronger Abs_eq_iff2 theorems changeset | files
2011-01-18 Christian Urban made alpha_abs_set_stronger1 stronger changeset | files
2011-01-18 Christian Urban removed finiteness assumption from set_rename_perm changeset | files
2011-01-18 Cezary Kaliszyk alpha_abs_set_stronger1 changeset | files
2011-01-18 Cezary Kaliszyk alpha_abs_let_stronger is not true in the same form changeset | files
2011-01-18 Christian Urban the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions changeset | files
2011-01-18 Christian Urban modified the renaming_perm lemmas changeset | files
2011-01-17 Christian Urban added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) changeset | files
2011-01-17 Christian Urban added a few examples of functions to Lambda.thy changeset | files
2011-01-17 Christian Urban exported nominal function code to external file changeset | files
2011-01-17 Christian Urban removed old testing code from Lambda.thy changeset | files
2011-01-17 Christian Urban moved high level code from LamTest into the main libraries. changeset | files
2011-01-17 Christian Urban eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation changeset | files
2011-01-15 Christian Urban subst also works now changeset | files
2011-01-15 Christian Urban nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions changeset | files
2011-01-14 Christian Urban strengthened renaming lemmas changeset | files
2011-01-13 Christian Urban added eqvt_lemmas for subset and psubset changeset | files
2011-01-10 Christian Urban a few lemmas about freshness for at and at_base changeset | files
2011-01-10 Christian Urban added a property about finite support in the presense of eqvt_at changeset | files
2011-01-09 Christian Urban instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis changeset | files
2011-01-09 Christian Urban solved subgoals for depth and subst function changeset | files
2011-01-09 Christian Urban added eqvt_at premises in function definition - however not proved at the moment changeset | files
2011-01-07 Christian Urban added one further lemma about equivariance of THE_default changeset | files
2011-01-07 Christian Urban equivariance of THE_default under the uniqueness assumption changeset | files
2011-01-07 Christian Urban derived equivariance for the function graph and function relation changeset | files
2011-01-06 Christian Urban a modified function package where, as a test, True has been injected into the compatibility condictions changeset | files
2011-01-06 Christian Urban removed last traces of debugging code changeset | files
2011-01-06 Christian Urban removed debugging code abd introduced a guarded tracing function changeset | files
2011-01-06 Christian Urban moved Weakening up....it does not compile when put at the last position changeset | files
2011-01-06 Christian Urban tuned changeset | files
2011-01-06 Christian Urban added weakening to the test cases changeset | files
2011-01-06 Christian Urban cleaned up weakening proof and added a version with finit sets changeset | files
2011-01-06 Christian Urban same changeset | files
2011-01-06 Christian Urban some further lemmas for fsets changeset | files
2011-01-06 Christian Urban made sure the raw datatypes and raw functions do not get any mixfix syntax changeset | files
2011-01-05 Christian Urban exported the code into a separate file changeset | files
2011-01-05 Christian Urban strong rule inductions; as an example the weakening lemma works changeset | files
2011-01-04 Christian Urban final version of the ESOP paper; used set+ instead of res as requested by one reviewer changeset | files
2011-01-03 Christian Urban file with most of the strong rule induction development changeset | files
2011-01-03 Christian Urban simple cases for string rule inductions changeset | files
2010-12-31 Christian Urban changed res keyword to set+ for restrictions; comment by a referee changeset | files
2010-12-31 Christian Urban added proper case names for all induct and exhaust theorems changeset | files
2010-12-31 Christian Urban added small example for strong inductions; functions still need a sorry changeset | files
2010-12-30 Christian Urban removed local fix for bug in induction_schema; added setup method for strong inductions changeset | files
2010-12-28 Christian Urban automated all strong induction lemmas changeset | files
2010-12-28 Christian Urban proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML changeset | files
2010-12-26 Christian Urban generated goals for strong induction theorems. changeset | files
2010-12-23 Christian Urban test with strong inductions changeset | files
2010-12-23 Christian Urban moved all strong_exhaust code to nominal_dt_quot; tuned examples changeset | files
2010-12-23 Christian Urban moved generic functions into nominal_library changeset | files
2010-12-22 Christian Urban slight tuning changeset | files
2010-12-22 Christian Urban slight tuning changeset | files
2010-12-22 Christian Urban tuned examples changeset | files
2010-12-22 Christian Urban added fold_right which produces the correct term for left-infix operators changeset | files
2010-12-22 Christian Urban updated to Isabelle 22 December changeset | files
2010-12-22 Christian Urban a bit tuning changeset | files
2010-12-22 Christian Urban corrected premises of strong exhausts theorems changeset | files
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples changeset | files
2010-12-21 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code changeset | files
2010-12-19 Christian Urban one interesting case done changeset | files
2010-12-19 Christian Urban a stronger statement for at_set_avoiding changeset | files
2010-12-17 Christian Urban tuned changeset | files
2010-12-17 Christian Urban tuned changeset | files
2010-12-16 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there changeset | files
2010-12-16 Christian Urban added theorem-rewriter conversion changeset | files
2010-12-14 Christian Urban freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through) changeset | files
2010-12-12 Christian Urban created strong_exhausts terms changeset | files
2010-12-12 Christian Urban moved setify and listify functions into the library; introduced versions that have a type argument changeset | files
2010-12-10 Christian Urban updated changeset | files
2010-12-09 Christian Urban a bit more tuning of the paper changeset | files
2010-12-09 Christian Urban brought the paper to 20 pages plus one page appendix changeset | files
2010-12-08 Christian Urban first tests about exhaust changeset | files
2010-12-08 Christian Urban moved some code into the nominal_library changeset | files
2010-12-08 Christian Urban moved definition of raw bn-functions into nominal_dt_rawfuns changeset | files
2010-12-08 Christian Urban kept the nested structure of constructors (belonging to one datatype) changeset | files
2010-12-07 Christian Urban moved general theorems into the libraries changeset | files
2010-12-07 Christian Urban automated permute_bn theorems changeset | files
2010-12-07 Christian Urban updated to changes in Isabelle changeset | files
2010-12-06 Christian Urban deleted nominal_dt_supp.ML changeset | files
2010-12-06 Christian Urban moved code from nominal_dt_supp to nominal_dt_quot changeset | files
2010-12-06 Christian Urban automated alpha_perm_bn theorems changeset | files
2010-12-06 Christian Urban ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof changeset | files
2010-12-03 Christian Urban updated to Isabelle 2nd December changeset | files
2010-11-29 Christian Urban isarfied some of the high-level proofs changeset | files
2010-11-29 Christian Urban added abs_rename_res lemma changeset | files
2010-11-29 Christian Urban completed proofs in Foo2 changeset | files
2010-11-28 Christian Urban completed the strong exhausts rules for Foo2 using general lemmas changeset | files
2010-11-27 Christian Urban tuned proof to reduce number of warnings changeset | files
2010-11-27 Christian Urban disabled the Foo examples, because of heavy work changeset | files
2010-11-26 Christian Urban slightly simplified the Foo2 tests and hint at a general lemma changeset | files
2010-11-26 Christian Urban completely different method fro deriving the exhaust lemma changeset | files
2010-11-26 Christian Urban merged changeset | files
2010-11-25 Christian Urban merged changeset | files
2010-11-24 Christian Urban added example from the F-ing paper by Rossberg, Russo and Dreyer changeset | files
2010-11-24 Christian Urban implemented concrete suggestion of 3rd reviewer changeset | files
2010-11-26 Cezary Kaliszyk missing freshness assumptions changeset | files
2010-11-25 Cezary Kaliszyk foo2 strong induction changeset | files
2010-11-24 Cezary Kaliszyk foo2 full exhausts changeset | files
2010-11-24 Cezary Kaliszyk Foo2 strong_exhaust for first variable. changeset | files
2010-11-22 Cezary Kaliszyk single rename in let2 changeset | files
2010-11-22 Cezary Kaliszyk current isabelle changeset | files
2010-11-21 Christian Urban added example Foo2.thy changeset | files
2010-11-15 Christian Urban tuned example changeset | files
2010-11-15 Christian Urban proved that bn functions return a finite set changeset | files
2010-11-15 Christian Urban added a test for the various shallow binders changeset | files
2010-11-15 Christian Urban fixed bug in fv function where a shallow binder binds lists of names changeset | files
2010-11-14 Christian Urban merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy changeset | files
2010-11-14 Christian Urban deleted special Nominal2_FSet theory changeset | files
2010-11-14 Christian Urban moved rest of the lemmas from Nominal2_FSet to the TypeScheme example changeset | files
2010-11-14 Christian Urban moved most material fron Nominal2_FSet into the Nominal_Base theory changeset | files
2010-11-14 Christian Urban tuned example changeset | files
2010-11-14 Christian Urban lifted permute_bn simp rules changeset | files
2010-11-13 Christian Urban lifted permute_bn constants changeset | files
2010-11-13 Christian Urban respectfulness for permute_bn functions changeset | files
2010-11-12 Christian Urban automated permute_bn functions (raw ones first) changeset | files
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package changeset | files
2010-11-10 Christian Urban expanded the paper by uncommenting the comments and adding the appendix changeset | files
2010-11-07 Christian Urban fixed locally the problem with the function package; all tests work again changeset | files
2010-11-06 Christian Urban added a test about subtyping; disabled two tests, because of problem with function package changeset | files
2010-11-05 Christian Urban small typo changeset | files
2010-10-29 Christian Urban squeezed qpaper to 6 pages changeset | files
2010-10-29 Cezary Kaliszyk Qpaper / Move examples to commented out appendix changeset | files
2010-10-28 Cezary Kaliszyk Unanonymize qpaper changeset | files
2010-10-28 Cezary Kaliszyk FSet changes for Qpaper changeset | files
2010-10-28 Cezary Kaliszyk Remove FSet and use the one from Isabelle changeset | files
2010-10-19 Christian Urban took out comment about map-types / adapted to recent changes changeset | files
2010-10-19 Christian Urban use definitions instead of functions changeset | files
2010-10-18 Christian Urban tuned changeset | files
2010-10-18 Christian Urban used functions instead of definitions changeset | files
2010-10-18 Christian Urban added missing style file changeset | files
2010-10-18 Cezary Kaliszyk Use the generalized compositional quotient theorem changeset | files
2010-10-17 Christian Urban fixed typo changeset | files
2010-10-17 Christian Urban all tests work again changeset | files
2010-10-17 Christian Urban some tuning changeset | files
2010-10-17 Christian Urban naming scheme is now *_fset (not f*_) changeset | files
2010-10-15 Christian Urban more cleaning changeset | files
2010-10-15 Christian Urban further tuning changeset | files
2010-10-15 Christian Urban renamed fminus_raw to diff_list changeset | files
2010-10-15 Christian Urban renamed fcard_raw to card_list changeset | files
2010-10-15 Christian Urban slight update changeset | files
2010-10-15 Christian Urban Further reorganisation and cleaning changeset | files
2010-10-15 Christian Urban further cleaning changeset | files
2010-10-15 Christian Urban typo changeset | files
2010-10-15 Cezary Kaliszyk FSet: stronger fact in Isabelle. changeset | files
2010-10-15 Cezary Kaliszyk FSet synchronizing changeset | files
2010-10-15 Cezary Kaliszyk Synchronizing FSet further. changeset | files
2010-10-15 Cezary Kaliszyk Partially merging changes from Isabelle changeset | files
2010-10-14 Christian Urban fixed the typo in the abstract and the problem with append (the type of map_k changeset | files
2010-10-14 Christian Urban changed format of the pearl paper changeset | files
2010-10-14 Christian Urban deleted some unused lemmas changeset | files
2010-10-14 Christian Urban major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw) changeset | files
2010-10-13 Christian Urban more on the pearl paper changeset | files
2010-10-12 Christian Urban added a section about abstractions changeset | files
2010-10-12 Christian Urban tiny work on the pearl paper changeset | files
2010-10-08 Christian Urban tuned changeset | files
2010-10-08 Christian Urban added apendix to paper detailing one proof changeset | files
2010-10-08 Christian Urban minor changeset | files
2010-10-08 Christian Urban minor changeset | files
2010-10-08 Christian Urban down to 20 pages changeset | files
2010-10-07 Cezary Kaliszyk minor changeset | files
2010-10-06 Christian Urban down to 21 pages and changed strong induction section changeset | files
2010-10-06 Christian Urban tuned changeset | files
2010-10-06 Christian Urban down to 22 pages changeset | files
2010-10-05 Christian Urban down to 23 pages changeset | files
2010-10-05 Christian Urban down to 24 pages and a bit changeset | files
2010-10-05 Christian Urban llncs and more sqeezing changeset | files
2010-10-04 Christian Urban first part of sqeezing everything into 20 pages (at the moment we have 26) changeset | files
2010-10-04 Christian Urban changed to llncs changeset | files
2010-10-01 Christian Urban merged changeset | files
2010-10-01 Christian Urban minor experiments changeset | files
2010-09-30 Christian Urban merged changeset | files
2010-09-29 Christian Urban simplified exhaust proofs changeset | files
2010-10-01 Cezary Kaliszyk Made the paper to compile with the renamings. changeset | files
2010-09-29 Christian Urban merged changeset | files
2010-09-29 Christian Urban worked example Foo1 with induct_schema changeset | files
2010-09-29 Christian Urban merged changeset | files
2010-09-29 Christian Urban use also induct_schema for the Let-example (permute_bn is used) changeset | files
2010-09-29 Christian Urban test with induct_schema for simpler strong_ind proofs changeset | files
2010-09-29 Cezary Kaliszyk substitution definition with 'next_name'. changeset | files
2010-09-28 Christian Urban merged changeset | files
2010-09-28 Christian Urban added Foo1 to explore a contrived example changeset | files
2010-09-27 Christian Urban added postprocessed fresh-lemmas for constructors changeset | files
2010-09-27 Christian Urban post-processed eq_iff and supp threormes according to the fv-supp equality changeset | files
2010-09-27 Christian Urban more consistent naming in Abs.thy changeset | files
2010-09-27 Christian Urban some experiments changeset | files
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
(0) -1000 -240 +240 tip
nominal2