| Tue, 14 Sep 2010 19:38:44 +0200 | blanchet | use same hack as in "Async_Manager" to work around Proof General bug | changeset | files |
| Tue, 14 Sep 2010 19:38:18 +0200 | blanchet | export function | changeset | files |
| Tue, 14 Sep 2010 17:36:27 +0200 | blanchet | generalize proof reconstruction code; | changeset | files |
| Tue, 14 Sep 2010 17:23:16 +0200 | blanchet | tuning | changeset | files |
| Tue, 14 Sep 2010 16:34:26 +0200 | blanchet | handle relevance filter corner cases more gracefully; | changeset | files |
| Tue, 14 Sep 2010 16:33:38 +0200 | blanchet | remove more clutter related to old "fast_descrs" optimization | changeset | files |
| Tue, 14 Sep 2010 15:39:57 +0200 | blanchet | Sledgehammer should be called in "prove" mode; | changeset | files |