[isabelle-dev] NEWS: asynchronous print functions etc.

Makarius makarius at sketis.net
Fri Jul 19 23:54:46 CEST 2013

On Mon, 15 Jul 2013, Makarius wrote:

> * Strictly monotonic document update, without premature cancelation of
> running transactions that are still needed: avoid reset/restart of
> such command executions while editing.
> * Support for asynchronous print functions, as overlay to existing
> document content.
> * Support for automatic tools in HOL, which try to prove or disprove
> toplevel theorem statements.
> This refers to Isabelle/9437f440ef3f.

Isabelle/43e48bb554ba concludes a second round through all tools, 
including sledgehammer.

Now that the auto tools are longer constrained by the boring TTY loop, 
where the user typing very slowly new commands in a synchronous manner, 
things become more ambitious and might cause further surprises.  So far it 
looks quite good, though.


More information about the isabelle-dev mailing list