[isabelle-dev] Towards the Isabelle2014 release

[Jasmin Christian Blanchette]

Am 07.07.2014 um 11:38 schrieb Makarius <makarius at sketis.net>:

> You probably mean the defaults for the "Provers" in the Sledgehammer panel.  It is now a bit simpler in only providing some static default, which is made persistent on the editor side if you change that.
> 
> Adding "smt" there includes that prover, but by default the main SMT solver Z3 is not activated, and somehow its invokation via Sledgehammer does not inform the user about it.

The "smt" tactic was never meant to be specified as a prover for Sledgehammer; for this purpose, "z3" (or "cvc3" or "yices") is better, because it focuses on proof search and does not attempt yet to reconstruct the proof (which would be somewhat premature, since minimization has not taken place yet). Hence, its output is not very polished.

The reason why "smt" and its cousin "metis" are supported (and listed in the documentation) is because they may arise in a minimization command generated by Sledgehammer, e.g. "sledgehammer min [prover = smt] (...)". In this context, it is useful to use the real "metis" or "smt", because this guarantees that the end result will actually work.

I have now clarified the documentation (5e8317c5b689).

Jasmin