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