| Thu, 05 Nov 2009 16:43:57 +0100 | Cezary Kaliszyk | More functionality for lifting list.cases and list.recs. | file | diff | annotate |
| Thu, 05 Nov 2009 09:55:21 +0100 | Christian Urban | merged | file | diff | annotate |
| Thu, 05 Nov 2009 09:38:34 +0100 | Cezary Kaliszyk | Infrastructure for polymorphic types | file | diff | annotate |
| Wed, 04 Nov 2009 09:52:31 +0100 | Cezary Kaliszyk | Lifting 'fold1.simps(2)' and some cleaning. | file | diff | annotate |
| Tue, 03 Nov 2009 18:09:59 +0100 | Cezary Kaliszyk | Playing with alpha_refl. | file | diff | annotate |
| Tue, 03 Nov 2009 17:51:10 +0100 | Cezary Kaliszyk | Alpha.induct now lifts automatically. | file | diff | annotate |
| Tue, 03 Nov 2009 17:30:43 +0100 | Cezary Kaliszyk | merge | file | diff | annotate |
| Tue, 03 Nov 2009 17:30:27 +0100 | Cezary Kaliszyk | applic_prs | file | diff | annotate |
| Tue, 03 Nov 2009 16:51:33 +0100 | Christian Urban | simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated | file | diff | annotate |
| Tue, 03 Nov 2009 16:17:19 +0100 | Cezary Kaliszyk | Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP | file | diff | annotate |
| Tue, 03 Nov 2009 14:04:21 +0100 | Cezary Kaliszyk | Preparing infrastructure for general FORALL_PRS | file | diff | annotate |
| Mon, 02 Nov 2009 14:57:56 +0100 | Cezary Kaliszyk | Optimization | file | diff | annotate |
| Mon, 02 Nov 2009 11:51:50 +0100 | Cezary Kaliszyk | Map does not fully work yet. | file | diff | annotate |
| Mon, 02 Nov 2009 11:15:26 +0100 | Cezary Kaliszyk | Fixed quotdata_lookup. | 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 |
| Fri, 30 Oct 2009 18:31:06 +0100 | Cezary Kaliszyk | Regularization | file | diff | annotate |
| Fri, 30 Oct 2009 16:35:43 +0100 | Christian Urban | added some facts about fresh and support of lam | file | diff | annotate |
| Fri, 30 Oct 2009 15:52:47 +0100 | Cezary Kaliszyk | Lemmas about fv. | file | diff | annotate |
| Fri, 30 Oct 2009 15:35:42 +0100 | Christian Urban | changed the order of rfv and reformulated a3 with rfv | file | diff | annotate |
| Fri, 30 Oct 2009 15:32:04 +0100 | Christian Urban | merged | file | diff | annotate |
| Fri, 30 Oct 2009 15:28:44 +0100 | Christian Urban | added fv-function | file | diff | annotate |
| Fri, 30 Oct 2009 15:22:59 +0100 | Cezary Kaliszyk | The proper real_alpha | file | diff | annotate |
| Fri, 30 Oct 2009 12:22:03 +0100 | Cezary Kaliszyk | Cleaning also in Lam | file | diff | annotate |
| Thu, 29 Oct 2009 17:35:03 +0100 | Cezary Kaliszyk | Tried manually lifting real_alpha | file | diff | annotate |
| Thu, 29 Oct 2009 13:30:11 +0100 | Cezary Kaliszyk | More tests in Lam | file | diff | annotate |
| Thu, 29 Oct 2009 08:46:34 +0100 | Cezary Kaliszyk | Lifting of the 3 lemmas in LamEx | file | diff | annotate |
| Thu, 29 Oct 2009 08:06:49 +0100 | Cezary Kaliszyk | Fixed wrong CARD definition and removed the "Does not work anymore" comment. | file | diff | annotate |
| Thu, 29 Oct 2009 07:29:12 +0100 | Christian Urban | merged | file | diff | annotate |
| Wed, 28 Oct 2009 19:36:52 +0100 | Christian Urban | fixed the definition of alpha; this *breaks* some of the experiments | file | diff | annotate |
| Wed, 28 Oct 2009 18:08:38 +0100 | Cezary Kaliszyk | disambiguate ===> syntax | file | diff | annotate |
| Wed, 28 Oct 2009 17:38:37 +0100 | Cezary Kaliszyk | More cleaning in Lam code | file | diff | annotate |
| Wed, 28 Oct 2009 16:48:57 +0100 | Cezary Kaliszyk | Some cleaning | file | diff | annotate |
| Wed, 28 Oct 2009 16:05:59 +0100 | Cezary Kaliszyk | Fixes | file | diff | annotate |
| Wed, 28 Oct 2009 15:25:36 +0100 | Christian Urban | merged | file | diff | annotate |
| Wed, 28 Oct 2009 15:25:11 +0100 | Christian Urban | added infrastructure for defining lifted constants | file | diff | annotate |
| Wed, 28 Oct 2009 14:59:24 +0100 | Cezary Kaliszyk | First experiments with Lambda | file | diff | annotate |
| Tue, 27 Oct 2009 14:14:30 +0100 | Christian Urban | added equiv-thm to the quot_info | file | diff | annotate |
| Tue, 27 Oct 2009 11:43:02 +0100 | Christian Urban | added an example about lambda-terms | file | diff | annotate |