merged

introduced a generic alpha (but not sure whether it is helpful)

More in the LF example in the new nominal way, all is clear until support.

Fixed the induction problem + some more proofs.

equivariance of rfv and alpha.

Added the experiments with fun and function.

now also final step is proved - the supp of lambdas is now completely characterised

the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms

improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions

merged

general abstraction operator and complete characterisation of its support and freshness

Ported existing part of LF to new permutations and alphas.

attempt of a general abstraction operator

attempt to prove equivalence between alpha definitions

End of renaming.

Minor when looking at lam.distinct and lam.inject

Renamed Bexeq to Bex1_rel

Substracting bounds from free variables.

Improper interface for datatype and function packages and proper interface lateron.

merged

minor

test about supp/freshness for lam (old proofs work in principle - for single binders)

Recommited the changes for nitpick

Correct types which fixes the printing.

fv for subterms

Fix the problem with later examples. Maybe need to go back to textual specifications.

Some processing of variables in constructors to get free variables.

Parsing of the input as terms and types, and passing them as such to the function package.

Undid the parsing, as it is not possible with thy->lthy interaction.

merge