QuotScript.thy
2009-11-30 Cezary Kaliszyk More code cleaning
2009-11-30 Cezary Kaliszyk Code cleaning.
2009-11-28 Cezary Kaliszyk Finished and tested the new regularize
2009-11-28 Cezary Kaliszyk Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
2009-11-27 Cezary Kaliszyk Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-26 Christian Urban fixed QuotList
2009-11-26 Christian Urban changed left-res
2009-11-26 Cezary Kaliszyk Manually regularized akind_aty_atrm.induct
2009-11-13 Cezary Kaliszyk Still don't know how to do the proof automatically.
2009-10-31 Cezary Kaliszyk Automatic computation of application preservation and manually finished "alpha.induct". Slow...
2009-10-30 Cezary Kaliszyk Regularize for equalities and a better tactic. "alpha.cases" now lifts.
2009-10-28 Cezary Kaliszyk disambiguate ===> syntax
2009-10-28 Cezary Kaliszyk First experiments with Lambda
2009-10-26 Cezary Kaliszyk Finished COND_PRS proof.
2009-10-26 Cezary Kaliszyk Cleaning and fixing.
2009-10-24 Christian Urban proved the two lemmas in QuotScript (reformulated them without leading forall)
2009-10-24 Cezary Kaliszyk Finally completely lift the previously lifted theorems + clean some old stuff
2009-10-24 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before
2009-10-24 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before
2009-10-24 cek Better tactic and simplified the proof further
2009-10-23 Cezary Kaliszyk eqsubst_tac
2009-10-22 Cezary Kaliszyk Removed an assumption
2009-10-22 Cezary Kaliszyk The proof now including manually unfolded higher-order RES_FORALL_RSP.
2009-10-22 Cezary Kaliszyk The problems with 'abs' term.
2009-10-17 Cezary Kaliszyk Partial simplification of the proof
2009-10-16 Cezary Kaliszyk Symmetric version of REP_ABS_RSP
2009-10-16 Cezary Kaliszyk Progressing with the proof
2009-10-15 Cezary Kaliszyk A number of lemmas for REGULARIZE_TAC and regularizing card1.
2009-10-14 Cezary Kaliszyk Proving the proper RepAbs version
2009-10-14 Cezary Kaliszyk Manually regularized list_induct2
2009-08-11 Christian Urban initial commit
less more (0) tip