QuotScript.thy
Thu, 26 Nov 2009 12:21:47 +0100 Cezary Kaliszyk Manually regularized akind_aty_atrm.induct
Fri, 13 Nov 2009 19:32:12 +0100 Cezary Kaliszyk Still don't know how to do the proof automatically.
Sat, 31 Oct 2009 11:20:55 +0100 Cezary Kaliszyk Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Fri, 30 Oct 2009 19:03:53 +0100 Cezary Kaliszyk Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Wed, 28 Oct 2009 18:08:38 +0100 Cezary Kaliszyk disambiguate ===> syntax
Wed, 28 Oct 2009 14:59:24 +0100 Cezary Kaliszyk First experiments with Lambda
Mon, 26 Oct 2009 10:20:20 +0100 Cezary Kaliszyk Finished COND_PRS proof.
less more (0) -10 -7 tip