2010-01-26 Cezary Kaliszyk Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.
2010-01-26 Cezary Kaliszyk Sigma cleaning works with split_prs (still manual proof).
2010-01-26 Christian Urban tuned
2010-01-26 Christian Urban merged
2010-01-26 Christian Urban cleaning of QuotProd; a little cleaning of QuotList
2010-01-26 Christian Urban added prs and rsp lemmas for Inl and Inr
2010-01-25 Christian Urban used split_option_all lemma
2010-01-25 Christian Urban used the internal Option.map instead of custom option_map
2010-01-26 Cezary Kaliszyk Generalized split_prs and split_rsp
2010-01-26 Cezary Kaliszyk All eq_reflections apart from the one of 'id_apply' can be removed.
2010-01-26 Cezary Kaliszyk continued
2010-01-26 Cezary Kaliszyk More eqreflection/equiv cleaning.
2010-01-26 Cezary Kaliszyk more eq_reflection & other cleaning.
2010-01-26 Cezary Kaliszyk Removing more eq_reflections.
2010-01-25 Christian Urban ids *cannot* be object equalities
2010-01-25 Christian Urban re-inserted lemma in QuotList
2010-01-25 Christian Urban added prs and rsp lemmas for Some and None
2010-01-25 Christian Urban tuned proofs (mainly in QuotProd)
2010-01-25 Christian Urban properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
2010-01-25 Christian Urban renamed QuotScript to QuotBase
2010-01-25 Christian Urban cleaned some theorems
2010-01-24 Christian Urban test with splits
2010-01-23 Cezary Kaliszyk The alpha equivalence relations for structures in 'Terms'
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-22 Cezary Kaliszyk Proper alpha equivalence for Sigma calculus.
2010-01-21 Cezary Kaliszyk Changed fun_map and rel_map to definitions.
2010-01-21 Cezary Kaliszyk Lifted Peter's Sigma lemma with Ex1.
2010-01-21 Cezary Kaliszyk Automatic injection of Bexeq
2010-01-21 Cezary Kaliszyk Automatic cleaning of Bexeq<->Ex1 theorems.
2010-01-21 Cezary Kaliszyk Using Bexeq_rsp, and manually lifted lemma with Ex1.
2010-01-21 Cezary Kaliszyk Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.
2010-01-21 Cezary Kaliszyk The missing rule.
2010-01-21 Cezary Kaliszyk Ex1 -> Bex1 Regularization, Preparing Exeq.
2010-01-20 Cezary Kaliszyk Added the Sigma Calculus example
2010-01-20 Cezary Kaliszyk Better error messages for non matching quantifiers.
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-17 Christian Urban added permutation functions for the raw calculi
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
(0) -300 -100 -60 +60 +100 +300 +1000 tip