Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 13:01:23 +0100] rev 625
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 13:00:36 +0100] rev 624
Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 12:59:38 +0100] rev 623
Proper checked map_rsp.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 12:36:28 +0100] rev 622
Nitpick found a counterexample for one lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 11:59:16 +0100] rev 621
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 11:38:58 +0100] rev 620
It also regularizes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 11:28:04 +0100] rev 619
inj_repabs also works.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 11:20:01 +0100] rev 618
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 08 Dec 2009 11:17:56 +0100] rev 617
An example of working cleaning for lambda lifting. Still not sure why Babs helps.
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 04:21:14 +0100] rev 616
tuned
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 04:14:02 +0100] rev 615
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 01:25:43 +0100] rev 614
added a thm list for ids
Christian Urban <urbanc@in.tum.de> [Tue, 08 Dec 2009 01:00:21 +0100] rev 613
removed a fixme: map_info is now checked
Christian Urban <urbanc@in.tum.de> [Mon, 07 Dec 2009 23:45:51 +0100] rev 612
tuning of the code
Christian Urban <urbanc@in.tum.de> [Mon, 07 Dec 2009 21:54:14 +0100] rev 611
merged