More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.

Trying to define hom for the lifted type directly.

Proper alpha equivalence for Sigma calculus.

Changed fun_map and rel_map to definitions.

Lifted Peter's Sigma lemma with Ex1.

Automatic injection of Bexeq

Automatic cleaning of Bexeq<->Ex1 theorems.

Using Bexeq_rsp, and manually lifted lemma with Ex1.

Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.

The missing rule.

Ex1 -> Bex1 Regularization, Preparing Exeq.

Added the Sigma Calculus example

Better error messages for non matching quantifiers.

Statement of term1_hom_rsp

proved that the function is a function

term1_hom as a function

A version of hom with quantifiers.

added permutation functions for the raw calculi

fixed broken (partial) proof

used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on

liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals

added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions

tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely

merged

added free_variable function (do not know about the algorithm yet)

hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.

slight tuning of relation_error

Appropriate respects and a statement of the lifted hom lemma

recursion-hom for lambda

Incorrect version of the homomorphism lemma

trivial

tuned quotient_typ.ML

tuned quotient_def.ML and cleaned somewhat LamEx.thy

a few more lemmas...except supp of lambda-abstractions

removed one sorry

nearly all of the proof

right generalisation

First subgoal.

setup for strong induction

exported absrep_const for nitpick.

minor

Simplified matches_typ.

added bound-variable functions to terms

merged

added 3 calculi with interesting binding structure

produce defs with lthy, like prs and ids

Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.

Finished organising an efficient datastructure for qconst_info.

Undid changes from symtab to termtab, since we need to lookup specialized types.

Moved the matches_typ function outside a?d simplified it.

one more item in the list of Markus

Put relation_error as a separate function.

Better error message for definition failure.

merge

Stored Termtab for constant information.

merged

deleted SOLVED'

Removed the 'oops' in IntEx.

tuned

added SOLVED' which is now part of Isabelle....must be removed eventually