Sat, 16 Jan 2010 02:09:38 +0100 Christian Urban liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
Fri, 15 Jan 2010 17:09:36 +0100 Christian Urban added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
Fri, 15 Jan 2010 16:13:49 +0100 Christian Urban 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 Christian Urban merged
Fri, 15 Jan 2010 15:56:06 +0100 Christian Urban added free_variable function (do not know about the algorithm yet)
Fri, 15 Jan 2010 15:51:25 +0100 Cezary Kaliszyk hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
Fri, 15 Jan 2010 12:17:30 +0100 Christian Urban slight tuning of relation_error
(0) -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 tip