2010-04-19 Cezary Kaliszyk FSet is a semi-lattice
2010-04-19 Cezary Kaliszyk merge
2010-04-19 Cezary Kaliszyk Putting FSet in bot typeclass.
2010-04-19 Cezary Kaliszyk reorder
2010-04-19 Christian Urban merged
2010-04-19 Christian Urban small updates to the paper; remaining points in PAPER-TODO
2010-04-19 Cezary Kaliszyk sub_list definition and respects
2010-04-19 Cezary Kaliszyk Alternate list_eq and equivalence
2010-04-19 Cezary Kaliszyk Some new lemmas
2010-04-19 Cezary Kaliszyk More cleaning
2010-04-19 Cezary Kaliszyk remove more metis
2010-04-19 Cezary Kaliszyk more metis cleaning
2010-04-19 Cezary Kaliszyk Getting rid of 'metis'.
2010-04-19 Cezary Kaliszyk merge
2010-04-19 Cezary Kaliszyk Remove 'defer'.
2010-04-19 Christian Urban merged
2010-04-19 Christian Urban tuned proofs
2010-04-19 Cezary Kaliszyk 2 more lifted lemmas needed for second representation
2010-04-19 Cezary Kaliszyk Accept non-equality eqvt rules in support proofs.
2010-04-19 Cezary Kaliszyk merge
2010-04-19 Cezary Kaliszyk Locations of files in Parser
2010-04-19 Cezary Kaliszyk merge
2010-04-19 Cezary Kaliszyk minor FSet3 edits.
2010-04-18 Christian Urban tuned
2010-04-18 Christian Urban moved some general function into nominal_library.ML
2010-04-18 Christian Urban tuned; transformation functions now take a context, a thm and return a thm
2010-04-18 Christian Urban tuned
2010-04-18 Christian Urban equivariance for alpha_raw in CoreHaskell is automatically derived
2010-04-18 Christian Urban preliminary parser for perm_simp metod
2010-04-16 Christian Urban automatic proofs for equivariance of alphas
2010-04-16 Cezary Kaliszyk Finished proof in Lambda.thy
2010-04-16 Christian Urban merged
2010-04-16 Christian Urban attempt to manual prove eqvt for alpha
2010-04-16 Cezary Kaliszyk Lifting in Term4.
2010-04-16 Christian Urban some tuning of eqvt-infrastructure
2010-04-15 Christian Urban some tuning of proofs
2010-04-15 Christian Urban typo
2010-04-15 Christian Urban merged
2010-04-15 Christian Urban half of the pair-abs-equivalence
2010-04-15 Cezary Kaliszyk More on Manual/Trm4
2010-04-15 Cezary Kaliszyk alpha4_equivp and constant lifting.
2010-04-15 Cezary Kaliszyk alpha4_eqvt and alpha4_reflp
2010-04-15 Cezary Kaliszyk fv_eqvt in term4
2010-04-15 Cezary Kaliszyk Updating in Term4.
2010-04-15 Cezary Kaliszyk merge
2010-04-15 Cezary Kaliszyk Prove insert_rsp2
2010-04-15 Christian Urban merged
2010-04-15 Christian Urban changed header
2010-04-15 Cezary Kaliszyk Minor paper fixes.
2010-04-14 Christian Urban temporary fix for CoreHaskell
2010-04-14 Christian Urban deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk Fix the 'subscript' error.
2010-04-14 Christian Urban merged
2010-04-14 Christian Urban thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk Separate alpha_definition.
2010-04-14 Cezary Kaliszyk Fix spelling in theory header
2010-04-14 Cezary Kaliszyk Separate define_fv.
2010-04-14 Christian Urban tuned and removed dead code
2010-04-14 Christian Urban moved a couple of more functions to the library
2010-04-14 Christian Urban added a library for basic nominal functions; separated nominal_eqvt file
2010-04-14 Christian Urban merged
2010-04-14 Christian Urban first working version of the automatic equivariance procedure
2010-04-14 Cezary Kaliszyk Initial cleaning/reorganization in Fv.
2010-04-14 Christian Urban merged
2010-04-14 Christian Urban preliminary tests
2010-04-14 Christian Urban deleted test
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk merge part: delete_rsp
2010-04-14 Cezary Kaliszyk merge part1: none_memb_nil
2010-04-14 Christian Urban added header and more tuning
2010-04-14 Christian Urban more tuning
2010-04-14 Christian Urban tuned
2010-04-13 Cezary Kaliszyk Working FSet with additional lemmas.
2010-04-13 Cezary Kaliszyk Much more in FSet (currently non-working)
2010-04-13 Christian Urban made everything to compile
2010-04-12 Christian Urban merged
2010-04-12 Christian Urban some small tunings (incompleted work in Lambda.thy)
2010-04-12 Christian Urban moved equivariance of map into Nominal2_Eqvt file
2010-04-12 Christian Urban early ott paper
2010-04-12 Cezary Kaliszyk Porting lemmas from Quotient package FSet to new FSet.
2010-04-12 Christian Urban added alpha-caml paper
2010-04-12 Christian Urban implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
2010-04-11 Christian Urban fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
2010-04-11 Christian Urban folded changes from the conference version
2010-04-11 Christian Urban added TODO item about parser creating syntax for the wrong type
2010-04-11 Christian Urban corrected imports header
2010-04-11 Christian Urban tuned
2010-04-11 Christian Urban a few tests
2010-04-11 Christian Urban added eqvt rules that are more standard
2010-04-11 Christian Urban used warning instead of tracing (does not seem to produce stable output)
2010-04-11 Christian Urban added small ittems about equivaraince of alpha_gens and name of lam.perm
2010-04-11 Christian Urban added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
2010-04-09 Christian Urban changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
2010-04-09 Brian Huffman rewrite paragraph introducing equivariance, add citation to Pitts03
2010-04-09 Brian Huffman edit 'contributions' section so we do not just quote directly from the reviewer
2010-04-09 Christian Urban renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
2010-04-08 Christian Urban clarified comment about distinct lists in th efuture work section
2010-04-08 Christian Urban tuned type-schemes example
2010-04-08 Christian Urban updated (comment about weirdo example)
2010-04-08 Christian Urban check whether the "weirdo" example from the binding bestiary works with shallow binders
2010-04-08 Christian Urban properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
2010-04-08 Christian Urban merged
2010-04-08 Christian Urban some further changes
2010-04-08 Brian Huffman merged
2010-04-08 Brian Huffman change some wording in conclusion
2010-04-08 Brian Huffman remove extra word
2010-04-08 Christian Urban merged
2010-04-08 Christian Urban added new paper directory for further work
2010-04-08 Brian Huffman use qualified name as string in concrete atom example
2010-04-08 Brian Huffman merged
2010-04-08 Brian Huffman simplify instance proof
2010-04-08 Brian Huffman polish explanation of additive group syntax
2010-04-08 Christian Urban final version of the pearl paper
2010-04-07 Christian Urban my final version of the paper
2010-04-07 Christian Urban added an induction principle for permutations; removed add_perm construction
2010-04-06 Christian Urban isarfied proof about existence of a permutation list
2010-04-06 Christian Urban added reference to E. Gunter's work
2010-04-06 Christian Urban typos in paper
2010-04-04 Christian Urban separated general nominal theory into separate folder
2010-04-03 Christian Urban added README and moved examples into separate directory
2010-04-03 Christian Urban merged pearl paper with this repository; started litrature subdirectory
2010-04-02 Christian Urban submitted version (just in time ;o)
2010-04-02 Christian Urban first complete version (slightly less than 3h more to go)
2010-04-02 Christian Urban tuned
2010-04-02 Christian Urban tuned strong ind section
2010-04-02 Christian Urban polished infrastruct section
2010-04-02 Christian Urban completed lifting section
2010-04-02 Christian Urban more on the lifting section
2010-04-02 Christian Urban more on the strong induction section
2010-04-01 Christian Urban completed conclusion
2010-04-01 Christian Urban merged
2010-04-01 Christian Urban merged
2010-04-01 Christian Urban updated related work section
2010-04-01 Cezary Kaliszyk fv_fv_bn
2010-04-01 Cezary Kaliszyk Update fv_bn definition for bindings allowed in types for which bn is present.
2010-04-01 Cezary Kaliszyk fv_perm_bn
2010-04-01 Cezary Kaliszyk Minor formula fixes.
2010-04-01 Christian Urban fixed alpha_bn
2010-04-01 Christian Urban current state
2010-04-01 Christian Urban merged
2010-04-01 Christian Urban added alpha_bn definition
2010-04-01 Cezary Kaliszyk hfill for right aligning single table cells.
2010-04-01 Cezary Kaliszyk Cleaning the strong induction example.
2010-04-01 Cezary Kaliszyk minor
2010-04-01 Cezary Kaliszyk Fighting with space in displaying strong induction...
2010-04-01 Cezary Kaliszyk starting strong induction
2010-04-01 Cezary Kaliszyk General paper minor fixes.
2010-04-01 Cezary Kaliszyk Forgot to save before commit.
2010-04-01 Cezary Kaliszyk Let with multiple bindings.
2010-04-01 Cezary Kaliszyk Fill the space below the figure.
2010-04-01 Christian Urban last commit for now.
2010-04-01 Christian Urban more on the conclusion
2010-04-01 Christian Urban completed related work section
2010-04-01 Christian Urban more on the paper
2010-03-31 Christian Urban added an item about alpha-equivalence (the existential should be closer to the abstraction)
2010-03-31 Christian Urban polished everything up to TODO
2010-03-31 Christian Urban merged
2010-03-31 Christian Urban added alpha-definition for ~~ty
2010-03-31 Cezary Kaliszyk permute_bn
2010-03-31 Christian Urban abbreviations for \<otimes> and \<oplus>
2010-03-31 Christian Urban merged
2010-03-31 Christian Urban a test with let having multiple bodies
2010-03-31 Christian Urban polished and removed tys from bn-functions.
2010-03-31 Cezary Kaliszyk merge
2010-03-31 Cezary Kaliszyk More on paper
2010-03-31 Christian Urban started to polish alpha-equivalence section, but needs more work
2010-03-31 Christian Urban started with a related work section
2010-03-30 Christian Urban polished and added an example for fvars
2010-03-30 Christian Urban cleaned up the section about fv's
2010-03-30 Christian Urban tuned beginning of section 4
2010-03-30 Cezary Kaliszyk More on section 5.
2010-03-30 Cezary Kaliszyk More on section 5.
2010-03-30 Christian Urban merged
2010-03-30 Christian Urban removed "raw" distinction
2010-03-30 Cezary Kaliszyk More on Section 5
2010-03-30 Cezary Kaliszyk Beginning of section 5.
2010-03-30 Christian Urban merged
2010-03-30 Cezary Kaliszyk Avoid mentioning other nominal datatypes as it makes things too complicated.
2010-03-30 Christian Urban merged
2010-03-30 Cezary Kaliszyk close the missing parenthesis on both sides.
2010-03-30 Christian Urban merged
2010-03-30 Christian Urban changes to section 2
2010-03-30 Cezary Kaliszyk Clean alpha
2010-03-30 Cezary Kaliszyk clean fv_bn
2010-03-30 Cezary Kaliszyk alpha_bn
2010-03-30 Cezary Kaliszyk Change @{text} to @{term}
2010-03-30 Cezary Kaliszyk alpha
2010-03-30 Cezary Kaliszyk more
2010-03-30 Cezary Kaliszyk fv and fv_bn
2010-03-30 Christian Urban more of the paper
2010-03-29 Christian Urban merged
2010-03-29 Cezary Kaliszyk Updated strong induction to modified definitions.
2010-03-29 Cezary Kaliszyk Initial renaming
2010-03-29 Christian Urban small changes in the core-haskell spec
2010-03-29 Cezary Kaliszyk Update according to paper
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk Changed to Lists.
2010-03-29 Christian Urban clarified core-haskell example
2010-03-29 Christian Urban spell check
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk Abs_gen and Abs_let simplifications.
2010-03-29 Christian Urban more on the paper
2010-03-28 Christian Urban fixed a problem due to a change in type-def (needs new Isabelle)
2010-03-28 Christian Urban merged
2010-03-28 Christian Urban more on the paper
2010-03-28 Christian Urban got rid of the aux-function on the raw level, by defining it with function on the quotient level
2010-03-27 Cezary Kaliszyk Lets finally abstract lists.
2010-03-27 Cezary Kaliszyk Core Haskell can now use proper strings.
2010-03-27 Cezary Kaliszyk Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
2010-03-27 Cezary Kaliszyk Remove list_eq notation.
2010-03-27 Cezary Kaliszyk Get lifted types information from the quotient package.
2010-03-27 Cezary Kaliszyk Equivariance when bn functions are lists.
2010-03-27 Cezary Kaliszyk Accepts lists in FV.
2010-03-27 Cezary Kaliszyk Parsing of list-bn functions into components.
2010-03-27 Cezary Kaliszyk Automatically compute support if only one type of Abs is present in the type.
2010-03-27 Cezary Kaliszyk Manually proved TySch support; All properties of TySch now true.
2010-03-27 Cezary Kaliszyk Generalize Abs_eq_iff.
2010-03-27 Cezary Kaliszyk Minor fix.
2010-03-27 Cezary Kaliszyk New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
2010-03-27 Cezary Kaliszyk Initial proof modifications for alpha_res
2010-03-27 Cezary Kaliszyk merge
2010-03-27 Cezary Kaliszyk Fv/Alpha now takes into account Alpha_Type given from the parser.
2010-03-27 Cezary Kaliszyk Minor cleaning.
2010-03-27 Christian Urban merged
2010-03-27 Christian Urban more on the paper
2010-03-27 Cezary Kaliszyk Removed some warnings.
2010-03-26 Cezary Kaliszyk merge
2010-03-26 Cezary Kaliszyk Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.
2010-03-26 Christian Urban merged
2010-03-26 Christian Urban more on the paper
2010-03-26 Christian Urban simplification
2010-03-26 Cezary Kaliszyk merge
2010-03-26 Cezary Kaliszyk Describe 'nominal_datatype2'.
2010-03-26 Cezary Kaliszyk Fixed renamings.
2010-03-26 Christian Urban merged
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-26 Cezary Kaliszyk Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
2010-03-26 Cezary Kaliszyk Update cheats in TODO.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
2010-03-26 Cezary Kaliszyk Fix Manual/LamEx for experiments.
2010-03-25 Cezary Kaliszyk Proper bn_rsp, for bn functions calling each other.
2010-03-25 Cezary Kaliszyk Gathering things to prove by induction together; removed cheat_bn_eqvt.
2010-03-25 Cezary Kaliszyk Update TODO
2010-03-25 Cezary Kaliszyk Showed ACons_subst.
2010-03-25 Cezary Kaliszyk Only ACons_subst left to show.
2010-03-25 Cezary Kaliszyk Solved all boring subgoals, and looking at properly defning permute_bv
2010-03-25 Cezary Kaliszyk One more copy-and-paste in core-haskell.
2010-03-25 Cezary Kaliszyk Properly defined permute_bn. No more sorry's in Let strong induction.
2010-03-25 Cezary Kaliszyk Showed Let substitution.
2010-03-25 Cezary Kaliszyk Only let substitution is left.
2010-03-25 Cezary Kaliszyk further in the proof
2010-03-25 Cezary Kaliszyk trying to prove the string induction for let.
(0) -1000 -256 +256 +1000 tip