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

add missing .bib

merge

starting bibliography

merged

updated to new Isabelle (More_Conv -> Conv)

made this example to work again

merge

alpha_alphabn for bindings in a type under bn.

minor tuning

Ex4 does work, and I don't see the difference between the alphas.

slight tuning

somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms

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

tuned paper

tuned paper

tuned a bit the paper

started a new file for the parser to make some experiments

moved old parser and fv into attic

polished example

merged

tuned a bit the paper

Proper fv/alpha for multiple compound binders

SingleLetFoo with everything.

Fv for multiple binding functions

added a more instructive example - has some problems with fv though

added flip_eqvt and swap_eqvt to the equivariance lists

tuned the paper

properly declared outer keyword

added an example which goes outside our current speciifcation

made out of STEPS a configuration value so that it can be set individually in each file