Wed, 05 Sep 2012 11:08:18 +0200 | blanchet | fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case | changeset | files |
Wed, 05 Sep 2012 11:08:18 +0200 | blanchet | don't get confused by extraneous premisses | changeset | files |
Wed, 05 Sep 2012 11:08:18 +0200 | blanchet | added a check | changeset | files |