QuotMain.thy
2009-11-28 Cezary Kaliszyk Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
2009-11-28 Cezary Kaliszyk Merged comment
2009-11-28 Christian Urban some slight tuning of the apply-tactic
2009-11-28 Christian Urban annotated a proof with all steps and simplified LAMBDA_RES_TAC
2009-11-27 Christian Urban replaced FIRST' (map rtac list) with resolve_tac list
2009-11-27 Cezary Kaliszyk Simplifying arguments; got rid of trans2_thm.
2009-11-27 Cezary Kaliszyk Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-27 Cezary Kaliszyk More cleaning in QuotMain, identity handling.
2009-11-27 Christian Urban tuned
2009-11-27 Christian Urban some tuning
2009-11-27 Christian Urban simplified gen_frees_tac and properly named abstracted variables
2009-11-27 Christian Urban removed CHANGED'
2009-11-27 Christian Urban introduced a separate lemma for id_simps
2009-11-27 Christian Urban renamed inj_REPABS to inj_repabs_trm
2009-11-27 Christian Urban tuned comments and moved slightly some code
2009-11-27 Christian Urban renamed REGULARIZE to be regularize
2009-11-26 Christian Urban more tuning
2009-11-26 Christian Urban deleted get_fun_old and stuff
2009-11-26 Christian Urban recommited changes of comments
2009-11-26 Cezary Kaliszyk Merge Again
2009-11-26 Cezary Kaliszyk Merged
2009-11-26 Christian Urban tuned comments
2009-11-26 Christian Urban some diagnostic code for r_mk_comb
2009-11-26 Christian Urban merged
2009-11-26 Christian Urban test with monos
2009-11-25 Cezary Kaliszyk applic_prs
2009-11-25 Christian Urban polishing
2009-11-25 Christian Urban reordered the code
2009-11-25 Cezary Kaliszyk Moved exception handling to QuotMain and cleaned FSet.
2009-11-25 Christian Urban comments tuning and slight reordering
2009-11-25 Cezary Kaliszyk Merge
2009-11-25 Cezary Kaliszyk More moving from QuotMain to UnusedQuotMain
2009-11-25 Christian Urban deleted some obsolete diagnostic code
2009-11-25 Cezary Kaliszyk Removed unused things from QuotMain.
2009-11-25 Cezary Kaliszyk lambda_prs and cleaning the existing examples.
2009-11-25 Christian Urban fixed the problem with generalising variables; at the moment it is quite a hack
2009-11-24 Christian Urban changed unification to matching
2009-11-24 Christian Urban unification
2009-11-24 Cezary Kaliszyk Lambda & SOLVED' for new quotient_tac
2009-11-24 Christian Urban merged
2009-11-24 Christian Urban merged
2009-11-24 Christian Urban use error instead of raising our own exception
2009-11-24 Cezary Kaliszyk Fixes to the tactic after quotient_tac changed.
2009-11-24 Christian Urban merged
2009-11-24 Christian Urban added a prepare_tac
2009-11-24 Cezary Kaliszyk TRY' for clean_tac
2009-11-24 Cezary Kaliszyk Moved cleaning to QuotMain
2009-11-24 Cezary Kaliszyk New cleaning tactic
2009-11-24 Cezary Kaliszyk Separate regularize_tac
2009-11-24 Cezary Kaliszyk More fixes for inj_REPABS
2009-11-24 Christian Urban addded a tactic, which sets up the three goals of the `algorithm'
2009-11-23 Christian Urban fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
2009-11-23 Christian Urban tuned some comments
2009-11-23 Cezary Kaliszyk domain_type in regularizing equality
2009-11-23 Cezary Kaliszyk More theorems lifted in the goal-directed way.
2009-11-23 Cezary Kaliszyk Finished temporary goal-directed lift_theorem wrapper.
less more (0) -100 -56 tip