generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"

More about the general lifting procedure.

Update TODO

Progress with general lifting procedure.

RSP of perms can be shown in one go.

Change in signature of prove_const_rsp for general lifting.

Permutation and FV_Alpha interface change.

To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.

merge

Preparing the generalized lifting procedure

merged

added ott-example about Leroy96

Forgot to add one file.

Split Terms into separate files and add them to tests.

merge

Move the eqvt code out of Terms and fixed induction for single-rule examples.

merged

a few simplifications

first attempt to make sense out of the core-haskell definition

Code for proving eqvt, still in Terms.

Use eqvt infrastructure.

Simple function eqvt code.

added IsaMakefile...but so far included only a test for the parser

moved Quot package to Attic (still compiles there with "isabelle make")

merged

moved Nominal to "toplevel"

Export perm_frees.

Restructuring the code in Perm

Simplified and finised eqvt proofs for t1 and t5

merge

Define lifted perms.

merged

parsing and definition of raw datatype and bv-function work (not very beautiful)

With permute_rsp we can lift the instance proofs :).

Note the instance proofs, since they can be easily lifted.

More refactoring and removed references to the global simpset in Perm.

Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.

Regularize finite support proof for trm1

Made the fv-supp proof much more straightforward.

Regularize the proofs about finite support.

Respects of permute and constructors.

Generate fv_rsp automatically.

Define the constants automatically.

Rename also the lifted types to non-capital.

Use the infrastructure in LF. Much shorter :).

Final synchronization of names.

LF renaming part 3 (proper names of alpha equvalences)

LF renaming part 2 (proper fv functions)

merge

LF renaming part1.

merged

parsing of function definitions almost works now; still an error with undefined constants

merge

rsp for bv; the only issue is that it requires an appropriate induction principle.

merged

declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types

rsp infrastructure.

merge

Progress towards automatic rsp of constants and fv.

merged