| Wed, 05 Sep 2012 14:49:35 +0200 | traytel | do not trivialize important internal theorem in quick_and_dirty mode | changeset | files |
| Wed, 05 Sep 2012 13:44:03 +0200 | wenzelm | merged | changeset | files |
| Wed, 05 Sep 2012 11:37:22 +0200 | blanchet | made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation) | changeset | files |