Thu, 22 Oct 2009 17:35:40 +0200 | Cezary Kaliszyk | Further developing the tactic and simplifying the proof | file | diff | annotate |
Thu, 22 Oct 2009 16:24:02 +0200 | Cezary Kaliszyk | res_forall_rsp_tac further simplifies the proof | file | diff | annotate |
Thu, 22 Oct 2009 16:10:06 +0200 | Cezary Kaliszyk | Working on the proof and the tactic. | file | diff | annotate |
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 |