IntEx.thy
2009-12-01 Cezary Kaliszyk Cleaning 'aps'.
2009-11-30 Cezary Kaliszyk Code cleaning.
2009-11-29 Christian Urban tried to improve the inj_repabs_trm function but left the new part commented out
2009-11-29 Cezary Kaliszyk Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
2009-11-29 Christian Urban introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
2009-11-28 Christian Urban removed old inj_repabs_tac; kept only the one with (selective) debugging information
2009-11-28 Christian Urban renamed r_mk_comb_tac to inj_repabs_tac
2009-11-28 Cezary Kaliszyk Merged and tested that all works.
2009-11-28 Cezary Kaliszyk Finished and tested the new regularize
2009-11-28 Christian Urban fixed examples in IntEx and FSet
2009-11-28 Christian Urban fixed previous commit
2009-11-28 Christian Urban annotated a proof with all steps and simplified LAMBDA_RES_TAC
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 Minor cleaning
2009-11-27 Christian Urban introduced a separate lemma for id_simps
2009-11-27 Christian Urban deleted obsolete qenv code
2009-11-27 Christian Urban renamed REGULARIZE to be regularize
2009-11-25 Cezary Kaliszyk applic_prs
2009-11-25 Cezary Kaliszyk Removed unused things from QuotMain.
2009-11-25 Cezary Kaliszyk cleaning in MyInt
2009-11-25 Christian Urban fixed the problem with generalising variables; at the moment it is quite a hack
2009-11-24 Christian Urban added a prepare_tac
2009-11-24 Cezary Kaliszyk Moved cleaning to QuotMain
2009-11-24 Cezary Kaliszyk New cleaning tactic
2009-11-24 Christian Urban explicit phases for the cleaning
2009-11-24 Christian Urban addded a tactic, which sets up the three goals of the `algorithm'
2009-11-23 Cezary Kaliszyk Finished temporary goal-directed lift_theorem wrapper.
2009-11-23 Cezary Kaliszyk Fixes for atomize
2009-11-23 Cezary Kaliszyk lift_thm with a goal.
less more (0) -50 -30 tip