Wed, 05 Sep 2012 11:18:48 +0200 | blanchet | tuning (systematic 1-based indices) | changeset | files |
Wed, 05 Sep 2012 11:16:34 +0200 | blanchet | reindented code | changeset | files |
Wed, 05 Sep 2012 11:11:26 +0200 | blanchet | added TODO | changeset | files |
Wed, 05 Sep 2012 11:08:18 +0200 | blanchet | tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it | changeset | files |
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 |