Minor beutification.

Define the quotient from ML

All works in LF but will require renaming.

Reordering in LF.

Fixes for auxiliary datatypes.

Fixed pseudo_injectivity for trm4

Testing auto equivp code.

A tactic for final equivp

More equivp infrastructure.

tactify transp

export the reflp and symp tacs.

Generalize atom_trans and atom_sym.

Some progress about transp

alpha-symmetric addons.

alpha reflexivity

Renaming.

Added missing description.

Added Brian's suggestion.

Update TODO

Removed bindings 'in itself' where possible.

Some adaptation

proof cleaning and standardizing.

Automatic production and proving of pseudo-injectivity.

Experiments for the pseudo-injectivity tactic.

merge

Constructing alpha_inj goal.

merged

start work with the parser

Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.

First (non-working) version of alpha-equivalence

Description of the fv procedure.

Testing auto constant lifting.

Fix for new Isabelle (primrec)

Automatic lifting of constants.

Changed back to original version of trm5

The alternate version of trm5 with additional binding. All proofs work the same.

Code for handling atom sets.

Replace Terms by Terms2.

Fixed proofs in Terms2 and found a mistake in Terms.

Terms2 with bindings for binders synchronized with bindings they are used in.

Cleaning of proofs in Terms.

Testing Fv

Fix the strong induction principle.

Reorder

Add bindings of recursive types by free_variables.

Bindings adapted to multiple defined datatypes.

Reorganization

Now should work.

Some optimizations and fixes.

Simplified format of bindings.

Tested the Perm code; works everywhere in Terms.

Wrapped the permutation code.

Description of intended bindings.

Code for generating the fv function, no bindings yet.

merge

indent

merge

Simplifying perm_eq

merge

indenting