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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
