Quot/QuotMain.thy
2010-02-10 Cezary Kaliszyk lowercase locale
2010-02-10 Cezary Kaliszyk Changes from Makarius's code review + some noticed fixes.
2010-02-10 Cezary Kaliszyk Some cleaning of proofs.
2010-02-10 Cezary Kaliszyk more minor space and bracket modifications.
2010-02-06 Christian Urban some tuning
2010-02-05 Cezary Kaliszyk A proper version of the attribute
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
2009-12-13 Christian Urban managed to simplify apply_rsp
2009-12-12 Christian Urban tried to simplify apply_rsp_tac; failed at the moment; added some questions
2009-12-12 Christian Urban some trivial changes
2009-12-12 Christian Urban trivial cleaning of make_inst
2009-12-12 Christian Urban tried to improve test; but fails
2009-12-12 Christian Urban merged
2009-12-12 Christian Urban annotated some questions to the code; some simple changes
2009-12-12 Cezary Kaliszyk Answering the question in code.
2009-12-12 Christian Urban tuned code
2009-12-12 Christian Urban renamed quotient.ML to quotient_typ.ML
2009-12-11 Cezary Kaliszyk Merge + Added LarryInt & Fset3 to tests.
2009-12-11 Cezary Kaliszyk Renaming
2009-12-11 Christian Urban deleted struct_match by Pattern.match (fixes a problem in LarryInt)
2009-12-11 Christian Urban added Int example from Larry
2009-12-11 Christian Urban changed error message
2009-12-11 Christian Urban reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case
2009-12-10 Christian Urban added maps-printout and tuned some comments
2009-12-10 Cezary Kaliszyk Regularized the hard lemma.
2009-12-10 Cezary Kaliszyk Found the problem with ttt3.
2009-12-10 Cezary Kaliszyk minor
2009-12-10 Cezary Kaliszyk Moved Unused part of locale to Unused QuotMain.
2009-12-10 Christian Urban more tuning
2009-12-10 Christian Urban tuned
2009-12-10 Christian Urban simplified the instantiation of QUOT_TRUE in procedure_tac
2009-12-10 Christian Urban completed previous commit
2009-12-10 Christian Urban deleted DT/NDT diagnostic code
2009-12-09 Cezary Kaliszyk Code cleaning.
2009-12-09 Christian Urban tuned
2009-12-09 Cezary Kaliszyk merge
2009-12-09 Cezary Kaliszyk Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
2009-12-09 Christian Urban deleted make_inst3
2009-12-09 Christian Urban tuned
2009-12-09 Christian Urban tuned
2009-12-09 Christian Urban moved function and tuned comment
2009-12-09 Christian Urban improved fun_map_conv
2009-12-09 Cezary Kaliszyk Arbitrary number of fun_map_tacs.
2009-12-09 Cezary Kaliszyk Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
2009-12-08 Christian Urban tuned code
2009-12-08 Christian Urban implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges
2009-12-08 Christian Urban decoupled QuotProd from QuotMain and also started new cleaning strategy
2009-12-08 Christian Urban properly set up the prs_rules
2009-12-08 Christian Urban merged
2009-12-08 Christian Urban added preserve rules to the cleaning_tac
2009-12-08 Cezary Kaliszyk merge
2009-12-08 Cezary Kaliszyk cleaning.
2009-12-08 Christian Urban chnaged syntax to "lifting theorem"
2009-12-08 Christian Urban changed names of attributes
2009-12-08 Christian Urban merged
2009-12-08 Christian Urban added methods for the lifting_tac and the other tacs
2009-12-08 Cezary Kaliszyk make_inst3
2009-12-08 Cezary Kaliszyk trans2 replaced with equals_rsp_tac
2009-12-08 Cezary Kaliszyk Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
2009-12-08 Cezary Kaliszyk Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
2009-12-08 Christian Urban tuned
2009-12-08 Christian Urban the lift_tac produces a warning message if one of the three automatic proofs fails
2009-12-08 Christian Urban added a thm list for ids
2009-12-08 Christian Urban removed a fixme: map_info is now checked
2009-12-07 Christian Urban tuning of the code
2009-12-07 Christian Urban merged
2009-12-07 Christian Urban removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
2009-12-07 Cezary Kaliszyk Handling of errors in lambda_prs_conv.
2009-12-07 Christian Urban clarified the function examples
2009-12-07 Christian Urban first attempt to deal with Babs in regularise and cleaning (not yet working)
2009-12-07 Cezary Kaliszyk make_inst for lambda_prs where the second quotient is not identity.
2009-12-07 Cezary Kaliszyk List moved after QuotMain
2009-12-07 Christian Urban directory re-arrangement
less more (0) tip