2010-08-16 Christian Urban also able to lift the bn_defs
2010-08-16 Christian Urban added rsp-lemmas for alpha_bns
2010-08-16 Christian Urban cezary made the eq_iff lemmas to lift (still needs some infrastructure in quotient)
2010-08-16 Christian Urban pinpointed the problem
2010-08-16 Christian Urban modified the code for class instantiations (with help from Florian)
2010-08-15 Christian Urban defined qperms and qsizes
2010-08-15 Christian Urban simplified code
2010-08-14 Christian Urban improved code
2010-08-14 Christian Urban more experiments with lifting
2010-08-12 Christian Urban updated to Isabelle 12th Aug
2010-08-11 Christian Urban rsp for constructors
2010-08-11 Christian Urban updated to Isabelle 11 Aug
2010-08-11 Christian Urban added a function that transforms the helper-rsp lemmas into real rsp lemmas
2010-08-08 Christian Urban proved rsp-helper lemmas of size functions
2010-07-31 Christian Urban tuning
2010-07-31 Christian Urban further simplification with alpha_prove
2010-07-31 Christian Urban introduced a general alpha_prove method
2010-07-29 Christian Urban equivariance for size
2010-07-29 Christian Urban helper lemmas for rsp-lemmas
2010-07-27 Christian Urban tests
2010-07-27 Christian Urban cleaned up a bit Abs.thy
2010-07-27 Christian Urban fixed order of fold_union to make alpha and fv agree
2010-07-26 Christian Urban small cleaning
2010-07-25 Christian Urban added paper by james; some minor cleaning
2010-07-23 Christian Urban samll changes
2010-07-23 Christian Urban made compatible
2010-07-23 Christian Urban added
2010-07-22 Christian Urban updated to new Isabelle; made FSet more "quiet"
2010-07-20 Christian Urban merged
2010-07-19 Christian Urban minor
2010-07-19 Christian Urban minor polishing
2010-07-19 Christian Urban quote for a new paper
2010-07-19 Christian Urban corrected lambda-preservation theorem
2010-07-19 Christian Urban minor
2010-07-18 Christian Urban minor things on the paper
2010-07-18 Christian Urban merged
2010-07-18 Christian Urban minor things
2010-07-18 Christian Urban some test with quotient
2010-07-17 Christian Urban some minor changes
2010-07-17 Christian Urban changes suggested by Peter Homeier
2010-07-17 Christian Urban tests
2010-07-16 Christian Urban submitted version
2010-07-16 Christian Urban more paper
2010-07-16 Christian Urban more on the paper
2010-07-16 Christian Urban more on the paper
2010-07-15 Christian Urban a bit more to the paper
2010-07-14 Christian Urban more on the paper
2010-07-13 Christian Urban more on slides
2010-07-13 Christian Urban slides
2010-07-12 Christian Urban more on slides
2010-07-11 Christian Urban slides
2010-07-10 Christian Urban slides
2010-07-10 Christian Urban more on slides
2010-07-10 Christian Urban more on slides
2010-07-10 Christian Urban added material for slides
2010-07-09 Christian Urban fixed
2010-07-09 Christian Urban before examples
2010-07-09 Christian Urban finished alpha-section
2010-07-07 Christian Urban more on the paper
2010-07-07 Christian Urban more on the paper
2010-07-02 Christian Urban more on the paper
2010-07-02 Christian Urban finished fv-section
2010-07-01 Christian Urban more on the paper
2010-07-01 Christian Urban spell check
2010-06-30 Christian Urban more work on the paper
2010-06-29 Christian Urban removed an "eqvt"-warning
2010-06-28 Christian Urban more quotient-definitions
2010-06-28 Christian Urban slight cleaning
2010-06-27 Christian Urban fixed according to changes in quotient
2010-06-24 Christian Urban added definition of the quotient types
2010-06-24 Christian Urban fixed according to changes in quotient
2010-06-23 Christian Urban added comment about partial equivalence relations
2010-06-23 Christian Urban even further polishing of the qpaper
2010-06-23 Christian Urban polished paper again (and took out some claims about Homeier's package)
2010-06-23 Christian Urban some slight polishing on the paper
2010-06-23 Christian Urban merged cezary's changes
2010-06-23 Christian Urban whitespace
2010-06-23 Cezary Kaliszyk Un-do the second change to SingleLet.
2010-06-23 Cezary Kaliszyk merge
2010-06-23 Cezary Kaliszyk Changes for PER and list_all2 committed to Isabelle
2010-06-18 Cezary Kaliszyk changes for partial-equivalence quotient package
2010-06-23 Christian Urban deleted compose-lemmas in Abs (not needed anymore)
2010-06-23 Christian Urban deleted equivp_hack
2010-06-22 Christian Urban proved eqvip theorems for alphas
2010-06-22 Christian Urban cleaned up the FSet (noise was introduced by error)
2010-06-22 Christian Urban prove that alpha implies alpha_bn (needed for rsp proofs)
2010-06-21 Christian Urban further post-submission tuning
2010-06-21 Christian Urban merged with main line
2010-06-21 Christian Urban merged
2010-06-11 Christian Urban also symmetry
2010-06-10 Christian Urban merged
2010-06-10 Christian Urban premerge
2010-06-09 Christian Urban transitivity proofs done
2010-06-07 Christian Urban merged
2010-06-07 Christian Urban work on transitivity proof
2010-06-03 Christian Urban added uminus_eqvt
2010-06-03 Christian Urban fixed problem with eqvt proofs
2010-06-02 Christian Urban fixed problem with bn_info
2010-06-01 Christian Urban merged
2010-06-01 Christian Urban equivariance done
2010-06-01 Christian Urban smaller code for raw-eqvt proofs
2010-05-31 Christian Urban all raw definitions are defined using function
2010-05-27 Christian Urban merged
2010-05-27 Christian Urban intermediate state
2010-05-26 Christian Urban merged
2010-05-26 Christian Urban added FSet to the correct paper
2010-05-24 Christian Urban added slides
2010-05-24 Christian Urban tuned
2010-05-24 Christian Urban tuned
2010-05-24 Christian Urban alpha works now
2010-05-23 Christian Urban started to work on alpha
2010-05-22 Christian Urban properly exported bn_descr
2010-05-21 Christian Urban hving a working fv-definition without the export
2010-05-21 Christian Urban tuned
2010-05-20 Christian Urban proper parser for "exclude:"
2010-05-20 Christian Urban tuned
2010-05-20 Christian Urban moved some mk_union and mk_diff into the library
2010-05-20 Christian Urban new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
2010-06-21 Christian Urban some post-submission polishing
2010-06-20 Christian Urban added a few points that need to be looked at the next version of the qpaper
2010-06-20 Christian Urban eliminated a quot_thm flag
2010-06-20 Christian Urban fixed example
2010-06-20 Christian Urban small addition to the acknowledgement
2010-06-17 Cezary Kaliszyk qpaper / address FIXMEs.
2010-06-17 Cezary Kaliszyk forgot to save
2010-06-17 Cezary Kaliszyk Fix regularization. Two "FIXME" left in introduction. Minor spellings.
2010-06-16 Christian Urban polished everything and submitted
2010-06-16 Christian Urban conclusion done
(0) -1000 -128 +128 tip