Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | put the flat at the right place (to avoid exceptions) | changeset | files |
Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | fixed variable exporting problem | changeset | files |
Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | compile | changeset | files |
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 |