Fri, 23 Oct 2009 18:20:06 +0200 | Cezary Kaliszyk | Stronger tactic, simpler proof. | changeset | files |
Fri, 23 Oct 2009 16:34:20 +0200 | Cezary Kaliszyk | Split Finite Set example into separate file | changeset | files |
Fri, 23 Oct 2009 16:01:13 +0200 | Cezary Kaliszyk | eqsubst_tac | changeset | files |
Fri, 23 Oct 2009 11:24:43 +0200 | Cezary Kaliszyk | Trying to get a simpler lemma with the whole infrastructure | changeset | files |
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 |