Fri, 30 Apr 2010 13:58:35 +0200 | blanchet | identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!) | changeset | files |
Fri, 30 Apr 2010 09:36:45 +0200 | blanchet | added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) | changeset | files |
Thu, 29 Apr 2010 19:08:02 +0200 | blanchet | in "overlord" mode: ignore problem prefix specified in the .thy file | changeset | files |
Thu, 29 Apr 2010 19:07:36 +0200 | blanchet | uncomment code | changeset | files |