Fri, 15 Jan 2010 16:13:49 +0100 tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
Christian Urban <urbanc@in.tum.de> [Fri, 15 Jan 2010 16:13:49 +0100] rev 894
tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
Fri, 15 Jan 2010 15:56:25 +0100 merged
Christian Urban <urbanc@in.tum.de> [Fri, 15 Jan 2010 15:56:25 +0100] rev 893
merged
Fri, 15 Jan 2010 15:56:06 +0100 added free_variable function (do not know about the algorithm yet)
Christian Urban <urbanc@in.tum.de> [Fri, 15 Jan 2010 15:56:06 +0100] rev 892
added free_variable function (do not know about the algorithm yet)
Fri, 15 Jan 2010 15:51:25 +0100 hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 15 Jan 2010 15:51:25 +0100] rev 891
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
(0) -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 tip