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

completely ported

Another string in the specification.

Variable takes a 'name'.

merge

When commenting discovered a missing case of Babs->Abs regularization.

merged

mostly ported Terms.thy to new Nominal

merge

Commenting regularize

very rough example file for how nominal2 specification can be parsed

reordered cases in regularize (will be merged into two cases)

use of equiv_relation_chk in quotient_term