Quot/Examples/LamEx.thy
2010-01-24 Christian Urban test with splits
2010-01-23 Cezary Kaliszyk More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
2010-01-23 Cezary Kaliszyk Trying to define hom for the lifted type directly.
2010-01-20 Cezary Kaliszyk Statement of term1_hom_rsp
2010-01-20 Christian Urban proved that the function is a function
2010-01-20 Cezary Kaliszyk term1_hom as a function
2010-01-19 Cezary Kaliszyk A version of hom with quantifiers.
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 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
less more (0) -15 tip