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
(0) -1000 -112 +112 +1000 tip