Mon, 30 Nov 2009 12:14:20 +0100 |
Cezary Kaliszyk |
More code cleaning
|
file |
diff |
annotate
|
Mon, 30 Nov 2009 11:53:20 +0100 |
Cezary Kaliszyk |
Code cleaning.
|
file |
diff |
annotate
|
Sat, 28 Nov 2009 05:29:30 +0100 |
Cezary Kaliszyk |
Finished and tested the new regularize
|
file |
diff |
annotate
|
Sat, 28 Nov 2009 04:02:54 +0100 |
Cezary Kaliszyk |
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
|
file |
diff |
annotate
|
Fri, 27 Nov 2009 08:15:23 +0100 |
Cezary Kaliszyk |
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
|
file |
diff |
annotate
|
Thu, 26 Nov 2009 13:52:46 +0100 |
Christian Urban |
fixed QuotList
|
file |
diff |
annotate
|
Thu, 26 Nov 2009 13:46:00 +0100 |
Christian Urban |
changed left-res
|
file |
diff |
annotate
|
Thu, 26 Nov 2009 12:21:47 +0100 |
Cezary Kaliszyk |
Manually regularized akind_aty_atrm.induct
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 19:32:12 +0100 |
Cezary Kaliszyk |
Still don't know how to do the proof automatically.
|
file |
diff |
annotate
|
Sat, 31 Oct 2009 11:20:55 +0100 |
Cezary Kaliszyk |
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
|
file |
diff |
annotate
|
Fri, 30 Oct 2009 19:03:53 +0100 |
Cezary Kaliszyk |
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 18:08:38 +0100 |
Cezary Kaliszyk |
disambiguate ===> syntax
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 14:59:24 +0100 |
Cezary Kaliszyk |
First experiments with Lambda
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 10:20:20 +0100 |
Cezary Kaliszyk |
Finished COND_PRS proof.
|
file |
diff |
annotate
|
Mon, 26 Oct 2009 10:02:50 +0100 |
Cezary Kaliszyk |
Cleaning and fixing.
|
file |
diff |
annotate
|