QuotScript.thy
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
less more (0) -16 tip