Quot/QuotMain.thy
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
less more (0) -60 tip