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
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.
2010-01-11 Christian Urban started to adhere to Wenzel-Standard
2010-01-11 Cezary Kaliszyk Changing exceptions to 'try', part 1.
2010-01-11 Cezary Kaliszyk removed quotdata_lookup_type
2010-01-11 Cezary Kaliszyk Fix for testing matching constants in regularize.
2010-01-11 Christian Urban tuned previous commit further
2010-01-10 Christian Urban the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
2010-01-09 Christian Urban introduced separate match function
2010-01-09 Christian Urban removed obsolete equiv_relation and rnamed new_equiv_relation
2010-01-08 Cezary Kaliszyk New_relations, all works again including concat examples.
2010-01-08 Cezary Kaliszyk map and rel simps for all quotients; needed when changing the relations to aggregate ones.
2010-01-08 Cezary Kaliszyk id_simps needs to be taken out not used directly, otherwise the new lemmas are not there.
2010-01-08 Cezary Kaliszyk Experimients with fconcat_insert
2010-01-08 Cezary Kaliszyk Modifications for new_equiv_rel, part2
2010-01-08 Cezary Kaliszyk Modifictaions for new_relation.
2010-01-08 Cezary Kaliszyk Proved concat_empty.
2010-01-07 Cezary Kaliszyk Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
2010-01-07 Cezary Kaliszyk some cleaning.
2010-01-07 Cezary Kaliszyk First generalization.
2010-01-07 Cezary Kaliszyk The working proof of the special case.
2010-01-07 Cezary Kaliszyk Reduced the proof to two simple but not obvious to prove facts.
2010-01-07 Cezary Kaliszyk More cleaning and commenting AbsRepTest. Now tests work; just slow.
2010-01-07 Cezary Kaliszyk cleaning in AbsRepTest.
2010-01-06 Cezary Kaliszyk Further in the proof
2010-01-06 Cezary Kaliszyk Tried to prove the lemma manually; only left with quotient proofs.
2010-01-06 Cezary Kaliszyk Sledgehammer bug.
2010-01-05 Cezary Kaliszyk merge
2010-01-05 Cezary Kaliszyk Trying the proof
2010-01-05 Christian Urban merged
2010-01-05 Cezary Kaliszyk Struggling with composition
2010-01-05 Cezary Kaliszyk Trying to state composition quotient.
2010-01-05 Christian Urban proper handling of error messages (code copy - maybe this can be avoided)
2010-01-05 Christian Urban added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
2010-01-05 Cezary Kaliszyk Readded 'regularize_to_injection' which I believe will be needed.
2010-01-02 Christian Urban added a warning to the quotient_type definition, if a map function is missing
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban a slight change to abs/rep generation
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban fixed comment errors
2010-01-01 Christian Urban some slight tuning
2009-12-31 Christian Urban renamed transfer to transform (Markus)
2009-12-30 cu some small changes
2009-12-27 Christian Urban added a functor that allows checking what is added to the theorem lists
2009-12-26 Christian Urban corrected wrong [quot_respect] attribute; tuned
2009-12-26 Christian Urban renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
2009-12-26 Christian Urban added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
2009-12-26 Christian Urban as expected problems occure when lifting concat lemmas
2009-12-26 Christian Urban tuned
(0) -120 +120 +1000 tip