Thu, 22 Oct 2009 16:24:02 +0200 | Cezary Kaliszyk | res_forall_rsp_tac further simplifies the proof | changeset | files |
Thu, 22 Oct 2009 16:10:06 +0200 | Cezary Kaliszyk | Working on the proof and the tactic. | changeset | files |
Thu, 22 Oct 2009 15:45:05 +0200 | Cezary Kaliszyk | The proof gets simplified | changeset | files |
Thu, 22 Oct 2009 15:44:16 +0200 | Cezary Kaliszyk | Removed an assumption | changeset | files |
Thu, 22 Oct 2009 15:02:01 +0200 | Cezary Kaliszyk | The proof now including manually unfolded higher-order RES_FORALL_RSP. | changeset | files |
Thu, 22 Oct 2009 13:45:48 +0200 | Cezary Kaliszyk | The problems with 'abs' term. | changeset | files |
Thu, 22 Oct 2009 11:43:12 +0200 | Cezary Kaliszyk | Simplified the proof with some tactic... Still hangs sometimes. | changeset | files |
Thu, 22 Oct 2009 10:45:33 +0200 | Cezary Kaliszyk | More proof | changeset | files |