| Sat, 24 Oct 2009 01:33:29 +0200 | Christian Urban | fixed problem with incorrect ABS/REP name | file | diff | annotate |
| Fri, 23 Oct 2009 16:34:20 +0200 | Cezary Kaliszyk | Split Finite Set example into separate file | file | diff | annotate |
| Fri, 23 Oct 2009 16:01:13 +0200 | Cezary Kaliszyk | eqsubst_tac | file | diff | annotate |
| 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 |