| Fri, 23 Oct 2009 11:24:43 +0200 | Cezary Kaliszyk | Trying to get a simpler lemma with the whole infrastructure | file | diff | annotate |
| Fri, 23 Oct 2009 09:21:45 +0200 | Cezary Kaliszyk | Using RANGE tactical allows getting rid of the quotients immediately. | file | diff | annotate |
| 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 |