Generalized the eqvt proof for single binders.

With induct instead of induct_tac, just one induction is sufficient.

General alpha_gen_trans for one-variable abstraction.

With unfolding Rep/Abs_eqvt no longer needed.

Lam2 finished apart from Rep_eqvt.

merge

All should be ok now.

repaired according to changes in Abs.thy

added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case

cleaned

updated from huffman

updated from nominal-huffman

Fixed wrong rename.

merge

Lambda based on alpha_gen, under construction.

updated from huffman - repo

renamed Abst/abst to Abs/abs

got rid of RAbst type - is now just pairs

Monotonicity of ~~gen, needed for using it in inductive definitions.

The current state of fv vs supp proofs in LF.

merge

More proofs in the LF example.

merged

slight tuning

renamed function according to the name of the constant

fixed problem with Bex1_rel renaming

Ported LF to the generic lambda and solved the simpler _supp cases.

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

Some cleaning of thy vs lthy vs context.

merged

tuned comment