Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | added induct tactic | changeset | files |
Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | tuning | changeset | files |
Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | renamed "mk_UnN" to "mk_UnIN" | changeset | files |
Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | merged two commands | changeset | files |
Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler) | changeset | files |
Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | distinguish between nested and nesting BNFs | changeset | files |