| Thu, 16 Sep 2010 09:59:32 +0200 | blanchet | prevent exception when calling "Mirabelle.can_apply" on empty proof sequence; | changeset | files |
| Thu, 16 Sep 2010 08:29:50 +0200 | blanchet | supply the Metis parameter defaults as argument, instead of patching the Metis sources; | changeset | files |
| Thu, 16 Sep 2010 08:27:10 +0200 | blanchet | regenerated "metis.ML" | changeset | files |