[isabelle-dev] NEWS: Z3 open source

[Makarius]

On Wed, 8 Apr 2015, Jasmin Blanchette wrote:

>  - Z3 is now always enabled by default, now that it is fully open
>    source. The "z3_non_commercial" option is discontinued.
>
> In addition, Z3 should now (again) be invoked by default by 
> Sledgehammer. Let me know if you see anything odd, e.g. odd problems 
> with binaries on Linux or Windows.

What is still not clear to me is how provers are determined.  The 
Sledgehammer panel uses the system option "sledgehammer_provers", after 
many failed attempts in the past to cope with the ML heuristics.  In 
Isabelle/323feed18a92 I've tried to update this wrt. recent changes.  Is 
it true that E prover now has this low priority in the list?  It was once 
first, IIRC.


Moreover, in Isabelle/dda1e781c7b4 I've updated the NEWS to say explicitly 
that the scheduling for provers managed by the Sledgehammer panel should 
now work better wrt. ongoing edits.  Despite such routine improvements, 
many users will probably just stick to old habits from the TTY age, and 
put the sledgehammer command into the text. (Are there remaining uses of 
this ancient form? Or are there still pending problems with the current 
Sledgehammer panel?)

BTW, the Sledgehammer manual still describes a situation before the 
Sledgehammer panel came into existance in 2013.  (It mentions the earlier 
Auto Sledgehammer in PIDE, though.)


 	Makarius