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

merged

tuned

absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"

More indenting, bracket removing and comment restructuring.

Finished replacing OO by OOO

Change OO to OOO in FSet3.

minor comment editing

modifying comments/indentation in quotient_term.ml

Cleaning comments, indentation etc in quotient_tacs.

No more exception handling in rep_abs_rsp_tac

handle all is no longer necessary in lambda_prs.

removed 3 hacks.

Updated some comments.

merge

Removed exception handling from equals_rsp_tac.