2010-01-16 Christian Urban fixed broken (partial) proof
2010-01-16 Christian Urban used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
2010-01-16 Christian Urban 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
2010-01-15 Christian Urban 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
2010-01-15 Christian Urban tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
2010-01-15 Christian Urban merged
2010-01-15 Christian Urban added free_variable function (do not know about the algorithm yet)
2010-01-15 Cezary Kaliszyk hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
2010-01-15 Christian Urban slight tuning of relation_error
2010-01-15 Cezary Kaliszyk Appropriate respects and a statement of the lifted hom lemma
2010-01-15 Christian Urban recursion-hom for lambda
2010-01-15 Cezary Kaliszyk Incorrect version of the homomorphism lemma
2010-01-14 Christian Urban trivial
2010-01-14 Christian Urban tuned quotient_typ.ML
2010-01-14 Christian Urban tuned quotient_def.ML and cleaned somewhat LamEx.thy
2010-01-14 Christian Urban a few more lemmas...except supp of lambda-abstractions
2010-01-14 Christian Urban removed one sorry
2010-01-14 Christian Urban nearly all of the proof
2010-01-14 Christian Urban right generalisation
2010-01-14 Cezary Kaliszyk First subgoal.
2010-01-14 Christian Urban setup for strong induction
2010-01-14 Cezary Kaliszyk exported absrep_const for nitpick.
2010-01-14 Cezary Kaliszyk minor
2010-01-14 Cezary Kaliszyk Simplified matches_typ.
2010-01-14 Christian Urban added bound-variable functions to terms
2010-01-14 Christian Urban merged
2010-01-14 Christian Urban added 3 calculi with interesting binding structure
2010-01-14 Cezary Kaliszyk produce defs with lthy, like prs and ids
2010-01-14 Cezary Kaliszyk Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
2010-01-14 Cezary Kaliszyk Finished organising an efficient datastructure for qconst_info.
2010-01-14 Cezary Kaliszyk Undid changes from symtab to termtab, since we need to lookup specialized types.
2010-01-13 Cezary Kaliszyk Moved the matches_typ function outside a?d simplified it.
2010-01-13 Christian Urban one more item in the list of Markus
2010-01-13 Cezary Kaliszyk Put relation_error as a separate function.
2010-01-13 Cezary Kaliszyk Better error message for definition failure.
2010-01-13 Cezary Kaliszyk merge
2010-01-13 Cezary Kaliszyk Stored Termtab for constant information.
2010-01-13 Christian Urban merged
2010-01-13 Christian Urban deleted SOLVED'
2010-01-13 Cezary Kaliszyk Removed the 'oops' in IntEx.
2010-01-13 Christian Urban tuned
2010-01-13 Christian Urban added SOLVED' which is now part of Isabelle....must be removed eventually
2010-01-13 Christian Urban merged
2010-01-12 Christian Urban tuned
2010-01-12 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
2010-01-12 Cezary Kaliszyk More indenting, bracket removing and comment restructuring.
2010-01-12 Cezary Kaliszyk Finished replacing OO by OOO
2010-01-12 Cezary Kaliszyk Change OO to OOO in FSet3.
2010-01-12 Cezary Kaliszyk minor comment editing
2010-01-12 Cezary Kaliszyk modifying comments/indentation in quotient_term.ml
2010-01-12 Cezary Kaliszyk Cleaning comments, indentation etc in quotient_tacs.
2010-01-12 Cezary Kaliszyk No more exception handling in rep_abs_rsp_tac
2010-01-12 Cezary Kaliszyk handle all is no longer necessary in lambda_prs.
2010-01-12 Cezary Kaliszyk removed 3 hacks.
2010-01-12 Cezary Kaliszyk Updated some comments.
2010-01-12 Cezary Kaliszyk merge
2010-01-12 Cezary Kaliszyk Removed exception handling from equals_rsp_tac.
2010-01-11 Christian Urban added an abbreviation for OOO
2010-01-11 Cezary Kaliszyk merge
2010-01-11 Cezary Kaliszyk Undid the non-working part.
(0) -300 -100 -60 +60 +100 +300 +1000 tip