| Thu, 22 Oct 2009 15:45:05 +0200 | Cezary Kaliszyk | The proof gets simplified | file | diff | annotate |
| Thu, 22 Oct 2009 15:02:01 +0200 | Cezary Kaliszyk | The proof now including manually unfolded higher-order RES_FORALL_RSP. | file | diff | annotate |
| Thu, 22 Oct 2009 13:45:48 +0200 | Cezary Kaliszyk | The problems with 'abs' term. | file | diff | annotate |
| Thu, 22 Oct 2009 11:43:12 +0200 | Cezary Kaliszyk | Simplified the proof with some tactic... Still hangs sometimes. | file | diff | annotate |