Quot/QuotMain.thy
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 All eq_reflections apart from the one of 'id_apply' can be removed.
2010-01-25 Christian Urban ids *cannot* be object equalities
2010-01-25 Christian Urban renamed QuotScript to QuotBase
2010-01-25 Christian Urban cleaned some theorems
2010-01-21 Cezary Kaliszyk Automatic injection of Bexeq
2010-01-21 Cezary Kaliszyk Using Bexeq_rsp, and manually lifted lemma with Ex1.
2010-01-21 Cezary Kaliszyk The missing rule.
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-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-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-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-08 Cezary Kaliszyk Modifictaions for new_relation.
2009-12-24 Christian Urban tuned
2009-12-23 Christian Urban renamed QUOT_TYPE to Quot_Type
2009-12-22 Christian Urban moved get_fun into quotient_term; this simplifies the overall including structure of the package
2009-12-22 Christian Urban tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
2009-12-21 Christian Urban get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
2009-12-17 Christian Urban minor cleaning
2009-12-17 Christian Urban moved the QuotMain code into two ML-files
2009-12-15 Cezary Kaliszyk lambda_prs & solve_quotient_assum cleaned.
2009-12-15 Christian Urban some commenting
2009-12-14 Cezary Kaliszyk Fixed previous commit.
2009-12-14 Cezary Kaliszyk Moved DETERM inside Repeat & added SOLVE around quotient_tac.
2009-12-14 Cezary Kaliszyk reply to question in code
2009-12-14 Cezary Kaliszyk Reply in code.
2009-12-13 Christian Urban a few code annotations
2009-12-13 Christian Urban another pass on apply_rsp
less more (0) -50 -30 tip