Fri, 23 Oct 2009 09:21:45 +0200 | Cezary Kaliszyk | Using RANGE tactical allows getting rid of the quotients immediately. | changeset | files |
Thu, 22 Oct 2009 17:35:40 +0200 | Cezary Kaliszyk | Further developing the tactic and simplifying the proof | changeset | files |
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 |