2010-05-27 Christian Urban merged
2010-05-27 Christian Urban fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
2010-05-27 Cezary Kaliszyk qpaper / lemmas used in proofs
2010-05-27 Cezary Kaliszyk qpaper / injection statement
2010-05-27 Cezary Kaliszyk qpaper / regularize
2010-05-27 Cezary Kaliszyk qpaper / a bit about prs
2010-05-27 Cezary Kaliszyk Functionalized the ABS/REP definition.
2010-05-26 Cezary Kaliszyk qpaper / lifting introduction
2010-05-26 Cezary Kaliszyk merged
2010-05-26 Christian Urban fixed compile error
2010-05-26 Cezary Kaliszyk qpaper / composition of quotients.
2010-05-26 Cezary Kaliszyk qpaper
2010-05-26 Cezary Kaliszyk qpaper..
2010-05-26 Cezary Kaliszyk qpaper.
2010-05-26 Cezary Kaliszyk Name some respectfullness
2010-05-26 Christian Urban added FSet to the correct paper
2010-05-26 Christian Urban merged
2010-05-26 Christian Urban added FSet
2010-05-26 Cezary Kaliszyk qpaper
2010-05-26 Cezary Kaliszyk qpaper
2010-05-25 Cezary Kaliszyk Substitution Lemma for TypeSchemes.
2010-05-25 Cezary Kaliszyk Simplified the proof
2010-05-25 Cezary Kaliszyk A lemma about substitution in TypeSchemes.
2010-05-25 Cezary Kaliszyk reversing the direction of fresh_star
2010-05-25 Cezary Kaliszyk overlapping deep binders proof
2010-05-25 Christian Urban edits from the reviewers
2010-05-24 Christian Urban tuned paper
2010-05-23 Christian Urban changed qpaper to lncs-style
2010-05-21 Cezary Kaliszyk Match_Lam defined on Quotient Level.
2010-05-21 Cezary Kaliszyk More on Function-defined subst.
2010-05-21 Cezary Kaliszyk Isabelle renamings
2010-05-21 Cezary Kaliszyk merge
2010-05-21 Cezary Kaliszyk Renamings.
2010-05-21 Cezary Kaliszyk Renamings
2010-05-21 Cezary Kaliszyk merge (non-trival)
2010-05-21 Cezary Kaliszyk Previously uncommited direct subst definition changes.
2010-05-21 Cezary Kaliszyk Function experiments
2010-05-19 Christian Urban merged
2010-05-19 Christian Urban added comments about pottiers work
2010-05-19 Cezary Kaliszyk more subst experiments
2010-05-19 Cezary Kaliszyk More subst experminets
2010-05-18 Cezary Kaliszyk more on subst
2010-05-18 Cezary Kaliszyk Single variable substitution
2010-05-18 Cezary Kaliszyk subst fix
2010-05-18 Cezary Kaliszyk subst experiments
2010-05-18 Christian Urban soem minor tuning
2010-05-18 Cezary Kaliszyk Fix broken add
2010-05-18 Cezary Kaliszyk add missing .bib
2010-05-18 Cezary Kaliszyk merge
2010-05-18 Cezary Kaliszyk starting bibliography
2010-05-17 Christian Urban merged
2010-05-17 Christian Urban updated to new Isabelle (More_Conv -> Conv)
2010-05-17 Christian Urban made this example to work again
2010-05-17 Cezary Kaliszyk merge
2010-05-17 Cezary Kaliszyk alpha_alphabn for bindings in a type under bn.
2010-05-17 Christian Urban minor tuning
2010-05-17 Cezary Kaliszyk Ex4 does work, and I don't see the difference between the alphas.
2010-05-17 Christian Urban slight tuning
2010-05-17 Christian Urban somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms
2010-05-16 Christian Urban moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
2010-05-16 Christian Urban tuned paper
2010-05-15 Christian Urban tuned paper
2010-05-14 Christian Urban tuned a bit the paper
2010-05-14 Christian Urban started a new file for the parser to make some experiments
2010-05-14 Christian Urban moved old parser and fv into attic
2010-05-14 Christian Urban polished example
2010-05-14 Christian Urban merged
2010-05-14 Christian Urban tuned a bit the paper
2010-05-14 Cezary Kaliszyk Proper fv/alpha for multiple compound binders
2010-05-14 Cezary Kaliszyk SingleLetFoo with everything.
2010-05-14 Cezary Kaliszyk Fv for multiple binding functions
2010-05-13 Christian Urban added a more instructive example - has some problems with fv though
2010-05-13 Christian Urban added flip_eqvt and swap_eqvt to the equivariance lists
2010-05-13 Christian Urban tuned the paper
2010-05-13 Christian Urban properly declared outer keyword
2010-05-13 Christian Urban added an example which goes outside our current speciifcation
2010-05-13 Christian Urban made out of STEPS a configuration value so that it can be set individually in each file
2010-05-13 Christian Urban tuned eqvt-proofs about prod_rel and prod_fv
2010-05-13 Christian Urban removed internal functions from the signature (they are not needed anymore)
2010-05-13 Christian Urban added term4 back to the examples
2010-05-13 Cezary Kaliszyk Make Term4 use 'equivariance'.
2010-05-12 Christian Urban fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
2010-05-12 Christian Urban merged
2010-05-12 Christian Urban moved the data-transformation into the parser
2010-05-12 Christian Urban added a test whether some of the constants already equivariant (then the procedure has to fail).
2010-05-12 Cezary Kaliszyk include set_simps and append_simps in fv_rsp
2010-05-12 Cezary Kaliszyk Move alpha_eqvt to unused.
2010-05-12 Cezary Kaliszyk Use equivariance instead of alpha_eqvt
2010-05-12 Cezary Kaliszyk merge
2010-05-12 Cezary Kaliszyk merge
2010-05-12 Cezary Kaliszyk fvbv_rsp include prod_rel.simps
2010-05-12 Christian Urban better ML-interface (returning only a list of theorems and a context)
2010-05-12 Cezary Kaliszyk merge
2010-05-12 Cezary Kaliszyk Use raw_induct instead of induct
2010-05-12 Christian Urban ingnored parameters in equivariance; added a proper interface to be called from ML
2010-05-12 Christian Urban properly exported defined bn-functions
2010-05-11 Cezary Kaliszyk Include raw permutation definitions in eqvt
2010-05-11 Cezary Kaliszyk Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
2010-05-11 Christian Urban a bit for the introduction of the q-paper
2010-05-11 Christian Urban added some of the quotient literature; a bit more to the qpaper
2010-05-10 Christian Urban fixed a problem with non-existant alphas2
2010-05-10 Christian Urban added comment about bind_set
2010-05-10 Christian Urban fixing bind_set problem
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Term8 comment
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Restore set bindings in CoreHaskell
2010-05-10 Cezary Kaliszyk Recursive examples with relation composition
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk prod_rel and prod_fv eqvt and mono
2010-05-10 Cezary Kaliszyk ExLetRec
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Parser changes for compound relations
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Use mk_compound_fv' and mk_compound_rel'
2010-05-10 Cezary Kaliszyk merge
2010-05-10 Cezary Kaliszyk Membership in a pair of lists.
2010-05-10 Cezary Kaliszyk Synchronize FSet with repository
2010-05-09 Christian Urban tuned file names for examples
2010-05-09 Christian Urban cleaned up a bit the examples; added equivariance to all examples
2010-05-09 Christian Urban fixed the problem with alpha containing splits
2010-05-09 Christian Urban added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
2010-05-07 Cezary Kaliszyk Manually added some newer keywords from the distribution
2010-05-07 Cezary Kaliszyk Regularize experiments
2010-05-06 Cezary Kaliszyk alpha_eqvt_tac with prod_rel and prod_fv simps
2010-05-06 Cezary Kaliszyk mem => member
2010-05-06 Cezary Kaliszyk merge
2010-05-06 Cezary Kaliszyk Fixes for new Isabelle
2010-05-06 Cezary Kaliszyk compound versions with prod_rel and prod_fun, not made default yet.
2010-05-06 Cezary Kaliszyk prod_rel and prod_fv simps
2010-05-06 Cezary Kaliszyk mem => member
2010-05-06 Cezary Kaliszyk prod_rel.simps and Fixed for new isabelle
2010-05-06 Cezary Kaliszyk Fixes for new isabelle
2010-05-06 Cezary Kaliszyk prod_fv and its respectfullness and preservation.
2010-05-06 Cezary Kaliszyk Experiments with equivariance.
2010-05-05 Christian Urban merged
2010-05-05 Christian Urban a bit mor on the pearl journal paper
2010-05-05 Christian Urban solved the problem with equivariance by first eta-normalising the goal
2010-05-05 Cezary Kaliszyk Some cleaning in Term4
2010-05-04 Cezary Kaliszyk "isabelle make" compiles all examples with newparser/newfv/newalpha only.
2010-05-04 Cezary Kaliszyk Move Term4 to NewParser
2010-05-04 Cezary Kaliszyk Fix Term4 for permutation signature change
2010-05-04 Cezary Kaliszyk Move LF to NewParser. Just works.
2010-05-04 Cezary Kaliszyk merge
2010-05-04 Cezary Kaliszyk ExLetMult
2010-05-04 Cezary Kaliszyk Ex1Rec.
2010-05-04 Cezary Kaliszyk merge
2010-05-04 Cezary Kaliszyk merge
2010-05-04 Cezary Kaliszyk ExPS3 in NewParser
2010-05-04 Cezary Kaliszyk Move ExPS8 to new parser.
2010-05-04 Cezary Kaliszyk Fix for new isabelle
2010-05-04 Cezary Kaliszyk merge
2010-05-04 Cezary Kaliszyk Minor
2010-05-04 Christian Urban increased step counter so that all steps go through
2010-05-04 Christian Urban fixed my error with define_raw_fv
2010-05-04 Christian Urban tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
2010-05-04 Cezary Kaliszyk Separate Term8, as it may work soon.
2010-05-04 Cezary Kaliszyk moved CoreHaskell to NewParser.
2010-05-04 Cezary Kaliszyk ExPS7 in NewParser
2010-05-04 Cezary Kaliszyk Move ExLeroy to New Parser
2010-05-04 Cezary Kaliszyk Move 2 more to NewParser
2010-05-04 Cezary Kaliszyk Move TypeSchemes to NewParser
2010-05-04 Cezary Kaliszyk Move ExLet to NewParser.
2010-05-04 Christian Urban tuned
2010-05-04 Christian Urban roll back of the last commit (there was a difference)
2010-05-04 Christian Urban tuned
2010-05-04 Christian Urban to my best knowledge the number of datatypes is equal to the length of the dt_descr; so we can save one argument in define_raw_perm
2010-05-04 Christian Urban merged
2010-05-04 Christian Urban some preliminary changes to the pearl-jv paper
2010-05-03 Christian Urban some preliminary notes of the abstract (qpaper); still need to see the motivating example
2010-05-03 Cezary Kaliszyk Added cheats to classical
2010-05-03 Cezary Kaliszyk Ex2 moved to new parser.
2010-05-03 Cezary Kaliszyk alpha_eqvt_tac fixed to work when the existential is not at the top level.
2010-05-03 Cezary Kaliszyk SingleLet and Ex3 work with NewParser.
2010-05-03 Cezary Kaliszyk Comment
2010-05-03 Cezary Kaliszyk Another example where only alpha_eqvt fails.
2010-05-03 Cezary Kaliszyk Register only non-looping rules in eq_iff
2010-05-03 Cezary Kaliszyk Equivariance fails for single let?
2010-05-03 Cezary Kaliszyk NewParser
2010-05-03 Cezary Kaliszyk Introduce eq_iff_simp to match the one from Parser.
2010-05-03 Cezary Kaliszyk remove tracing
2010-05-03 Cezary Kaliszyk Cheat support equations in new parser
2010-05-03 Cezary Kaliszyk Remove dependency on NewFv
2010-05-03 Cezary Kaliszyk Fix Parser
2010-05-03 Cezary Kaliszyk Add explicit cheats in NewParser and comment out the examples for outside use.
2010-05-03 Cezary Kaliszyk Fix Datatype_Aux calls in NewParser.
2010-05-03 Cezary Kaliszyk Move old fv_alpha_export to Fv.
2010-05-02 Christian Urban moved old parser and old fv back into their original places; isabelle make works again
2010-05-02 Christian Urban slight tuning
2010-05-02 Christian Urban simplified the supp-of-finite-sets proof
2010-05-02 Christian Urban tried to add some comments in the huge(!) nominal2_cmd function
2010-05-02 Christian Urban replaced make_pair with library function HOLogic.mk_prod
2010-05-02 Christian Urban removed duplicate eqvt attribute
2010-05-02 Christian Urban attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
2010-05-01 Christian Urban merged
2010-05-01 Christian Urban tuned
2010-04-30 Christian Urban replaced hide by the new hide_const
2010-04-30 Christian Urban generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
2010-04-30 Christian Urban added lemmas establishing the support of finite sets of finitely supported elements
2010-04-30 Christian Urban added eqvt-lemmas for Bex, Ball and Union
2010-04-30 Cezary Kaliszyk NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
2010-04-30 Cezary Kaliszyk Merged nominal_datatype into NewParser until eqvts
2010-04-30 Cezary Kaliszyk more parser/new parser synchronization.
2010-04-30 Cezary Kaliszyk Simplify old parser for integration
2010-04-30 Cezary Kaliszyk merge
2010-04-30 Cezary Kaliszyk Change signature of fv and alpha generation.
2010-04-30 Christian Urban reorganised eqvt-file (now uses perm_simp already)
2010-04-30 Cezary Kaliszyk qpaper
2010-04-29 Cezary Kaliszyk merge
2010-04-29 Cezary Kaliszyk New Alpha.
2010-04-29 Cezary Kaliszyk Minimal cleaning in LamEx
2010-04-29 Cezary Kaliszyk Remove things moved to the isabelle distribution
2010-04-29 Cezary Kaliszyk Unify and give only one name to 'setify', 'listify' and 'set'
2010-04-29 Cezary Kaliszyk Fixing the definitions in the Parser.
2010-04-29 Cezary Kaliszyk Some of the exceptions that the parser should check in TODO.
2010-04-29 Cezary Kaliszyk Extracting the fv body function and exporting the terms.
2010-04-29 Cezary Kaliszyk Fix for recursive binders.
2010-04-29 Cezary Kaliszyk revert 0c9ef14e9ba4
2010-04-29 Cezary Kaliszyk Support in positive position and atoms in negative positions.
2010-04-29 Cezary Kaliszyk merge
2010-04-29 Cezary Kaliszyk Include support of unknown datatypes in new fv
2010-04-29 Christian Urban merged
2010-04-29 Christian Urban added basic functions for constructing supp-terms
2010-04-29 Cezary Kaliszyk quotient paper
2010-04-29 Christian Urban added missing latex-style file
2010-04-29 Christian Urban merged
2010-04-29 Christian Urban added stub for quotient paper; call with isabelle make qpaper
2010-04-28 Cezary Kaliszyk Cleaning of Int and FSet Examples
2010-04-28 Christian Urban use the more general type-class at_base
2010-04-28 Christian Urban deleted left-over code
2010-04-28 Christian Urban simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
2010-04-28 Christian Urban use sort at_base instead of at
2010-04-28 Christian Urban white spaces
2010-04-28 Christian Urban avoided repeated dest of dt_info
2010-04-28 Christian Urban tuned
2010-04-28 Christian Urban factured out common functionality of prefixing the dt-names with a string
2010-04-28 Christian Urban closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
2010-04-27 Christian Urban added some further problemetic tests
2010-04-27 Christian Urban some tuning
2010-04-27 Christian Urban moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
2010-04-27 Christian Urban merged
2010-04-27 Cezary Kaliszyk Rewrote FV code and included the function package.
2010-04-27 Cezary Kaliszyk merge
2010-04-27 Cezary Kaliszyk Function in Core Haskell
2010-04-27 Christian Urban one more pass over the paper
2010-04-27 Christian Urban more polishing on the paper
2010-04-26 Christian Urban merged
2010-04-26 Christian Urban some changes to the paper
2010-04-26 Christian Urban rewrote eqvts_raw to be a symtab, that can be looked up
2010-04-26 Cezary Kaliszyk merge ???
2010-04-21 Cezary Kaliszyk infix for In
2010-04-26 Christian Urban eliminated command so that all compiles
2010-04-26 Christian Urban changed theorem_i to theorem....requires new Isabelle
2010-04-25 Christian Urban tuned
2010-04-25 Christian Urban tuned and cleaned
2010-04-25 Christian Urban tuned and made to compile
2010-04-25 Christian Urban added definition of raw-permutations to the new-parser
2010-04-25 Christian Urban tuned
2010-04-24 Christian Urban slight tuning
2010-04-24 Christian Urban added a comment about a function where I am not sure who wrote it.
2010-04-24 Christian Urban merged
2010-04-23 Cezary Kaliszyk Minor
2010-04-23 Cezary Kaliszyk Minor cleaning of IntEx
2010-04-23 Cezary Kaliszyk Further cleaning of proofs in FSet
2010-04-22 Cezary Kaliszyk Update term8
2010-04-22 Cezary Kaliszyk Converted 'thm' to a lemma.
2010-04-22 Cezary Kaliszyk Moved working Fset3 properties to FSet.
2010-04-22 Christian Urban tuned parser
2010-04-22 Christian Urban moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
2010-04-21 Christian Urban tuned proofs
2010-04-21 Christian Urban merged
2010-04-21 Christian Urban moved some lemmas into the right places
2010-04-21 Cezary Kaliszyk minor
2010-04-21 Cezary Kaliszyk merge
2010-04-21 Cezary Kaliszyk append_rsp2 + isarification
2010-04-21 Christian Urban some small changes
2010-04-21 Christian Urban merged
2010-04-21 Christian Urban deleted the incomplete proof about pairs of abstractions
2010-04-21 Christian Urban added a variant of the induction principle for permutations
2010-04-21 Cezary Kaliszyk merge
2010-04-21 Cezary Kaliszyk More about concat
2010-04-21 Christian Urban merged
2010-04-21 Christian Urban incomplete tests
2010-04-21 Christian Urban added an improved version of the induction principle for permutations
2010-04-21 Cezary Kaliszyk Working lifting of concat with inline proofs of second level preservation.
2010-04-21 Cezary Kaliszyk FSet3 cleaning part2
2010-04-21 Cezary Kaliszyk merge
2010-04-21 Cezary Kaliszyk Remove the part already in FSet and leave the experiments
2010-04-21 Christian Urban merged
2010-04-21 Christian Urban removed a sorry
2010-04-20 Christian Urban renamed Ex1.thy to SingleLet.thy
2010-04-20 Christian Urban tuning of the code
2010-04-21 Cezary Kaliszyk Reorder FSet
2010-04-21 Cezary Kaliszyk merge
2010-04-21 Cezary Kaliszyk lattice properties.
2010-04-20 Cezary Kaliszyk All lifted in Term4. Requires new isabelle.
2010-04-20 Cezary Kaliszyk fsets are distributive lattices.
2010-04-20 Cezary Kaliszyk Fix of comment
2010-04-20 Christian Urban reordered code
2010-04-20 Christian Urban renamed "_empty" and "_append" to "_zero" and "_plus"
2010-04-20 Christian Urban removed dead code (nominal cannot deal with argument types of constructors that are functions)
2010-04-20 Christian Urban added comment about abstraction in raw permuations
2010-04-20 Christian Urban optimised the code of define_raw_perm
2010-04-19 Christian Urban deleting function perm_arg in favour of the library function mk_perm
2010-04-19 Christian Urban merged
2010-04-19 Christian Urban tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
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.
(0) -1000 -480 +480 +1000 tip