[isabelle-dev] NEWS: sledgehammer panel

Makarius makarius at sketis.net
Sat Aug 17 15:41:01 CEST 2013

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Dockable window "Sledgehammer" manages asynchronous / parallel
sledgehammer runs over existing document sources, independently of
normal editing and checking process.

This refers to Isabelle/bca3769b6b45.  It should be usable already, 
although rounds 2 and 3 of refinements still need to be done before the 
coming release, to ensure that the multithreading and interrupting really 

All this has required a few years longer than anticipated. In 2005 Larry 
had proposed to make everything in Isabelle work concurrently, now we are 
more or less there.  It is now subsumed by the PIDE document model, and 
the implementation is not so big after all, probably smaller than the 
earlier isolated attempts taken together (e.g. the first multi-threaded 
ATP manager from summer 2008.)


More information about the isabelle-dev mailing list