updated to Isabelle 11 Aug

added a function that transforms the helper-rsp lemmas into real rsp lemmas

proved rsp-helper lemmas of size functions

tuning

further simplification with alpha_prove

introduced a general alpha_prove method

equivariance for size

helper lemmas for rsp-lemmas

tests

cleaned up a bit Abs.thy

fixed order of fold_union to make alpha and fv agree

small cleaning

added paper by james; some minor cleaning

samll changes

made compatible

added

updated to new Isabelle; made FSet more "quiet"

merged

minor

minor polishing

quote for a new paper

corrected lambda-preservation theorem

minor

minor things on the paper

merged

minor things

some test with quotient

some minor changes

changes suggested by Peter Homeier

tests

submitted version

more paper

more on the paper

more on the paper

a bit more to the paper

more on the paper

more on slides

slides

more on slides

slides

slides

more on slides

more on slides

added material for slides

fixed

before examples

finished alpha-section

more on the paper

more on the paper

more on the paper

finished fv-section

more on the paper

spell check

more work on the paper

removed an "eqvt"-warning

more quotient-definitions

slight cleaning

fixed according to changes in quotient

added definition of the quotient types

fixed according to changes in quotient

added comment about partial equivalence relations

even further polishing of the qpaper

polished paper again (and took out some claims about Homeier's package)

some slight polishing on the paper

merged cezary's changes

whitespace

Un-do the second change to SingleLet.

merge

Changes for PER and list_all2 committed to Isabelle

changes for partial-equivalence quotient package

deleted compose-lemmas in Abs (not needed anymore)

deleted equivp_hack

proved eqvip theorems for alphas

cleaned up the FSet (noise was introduced by error)

prove that alpha implies alpha_bn (needed for rsp proofs)

further post-submission tuning

merged with main line

merged

also symmetry

merged

premerge

transitivity proofs done

merged

work on transitivity proof

added uminus_eqvt

fixed problem with eqvt proofs

fixed problem with bn_info

merged

equivariance done

smaller code for raw-eqvt proofs

all raw definitions are defined using function

merged

intermediate state

merged

added FSet to the correct paper

added slides

tuned

tuned

alpha works now

started to work on alpha

properly exported bn_descr

hving a working fv-definition without the export

tuned

proper parser for "exclude:"

tuned

moved some mk_union and mk_diff into the library

new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files

some post-submission polishing

added a few points that need to be looked at the next version of the qpaper

eliminated a quot_thm flag

fixed example

small addition to the acknowledgement

qpaper / address FIXMEs.

forgot to save

Fix regularization. Two "FIXME" left in introduction. Minor spellings.

polished everything and submitted

conclusion done

Answer questions in comments

tuned

finished section 4, but put some things I do not understand on comment

4 almost finished

cleaned up definitions

merge

qpaper/Rewrite section5

merged

tuned everytinh up to section 4

Definition of Respects.

conclusion

Qpaper / Clarify the typing system and composition of quotients issue.

Remove only reference to 'equivp'.

merge

qpaper/ackno

tuned

qpaper

qpaper / hol4

qpaper/related work

finished preliminary section

typo

some slight tuning of the preliminary section

merge

qpaper

merged

tuned

Qpaper / beginnig of sec5

merge

qpaper/unfold the ball_reg_right statement

merged

some tuning and start work on section 4

qpaper

qpaper / INJ

qpaper / REG

qpaper / minor

qpaper/various

qpaper

qpaper/more on example

qpaper/examples

completed proof and started section about respectfulness and preservation

more on the qpaper

tuned

more on the constant lifting section

something about the quotient ype definitions

added some examples

improved definition of ABS and REP

qpaper.

some spelling

minor

qpaper / tuning in preservation and general display

polishing of ABS/REP

some slight tuning of the intro

Fix integer relation.

completed the intro (except minor things)

more intro

more on the qpaper

even more on the qpaper (intro almost done)

more to the introduction of the qpaper

adapted to the official sigplan style file (this gives us more space)

added to the popl-paper a pointer to work by Altenkirch

more on the qpaper

new title for POPL paper

more work on intro and abstract (done for today)

a bit more in the introduction and abstract

improved abstract, some tuning

Qpaper / minor on cleaning

qpaper / injection proof.

qpaper / example interaction

Qpaper/regularization proof.

qpaper

Qpaper/more.

Qpaper/Minor

added larry's quote

added larry's paper

tuned

first version of the abstract

merged

fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set

qpaper / lemmas used in proofs

qpaper / injection statement

qpaper / regularize

qpaper / a bit about prs

Functionalized the ABS/REP definition.

qpaper / lifting introduction

merged

fixed compile error

qpaper / composition of quotients.

qpaper

qpaper..

qpaper.

Name some respectfullness

added FSet to the correct paper

merged

added FSet

qpaper

qpaper

Substitution Lemma for TypeSchemes.

Simplified the proof

A lemma about substitution in TypeSchemes.

reversing the direction of fresh_star

overlapping deep binders proof

edits from the reviewers

tuned paper

changed qpaper to lncs-style

Match_Lam defined on Quotient Level.

More on Function-defined subst.

Isabelle renamings

merge

Renamings.

Renamings

merge (non-trival)

Previously uncommited direct subst definition changes.

Function experiments

merged

added comments about pottiers work

more subst experiments

More subst experminets

more on subst

Single variable substitution

subst fix

subst experiments

soem minor tuning

Fix broken add