[isabelle-dev] NEWS

Makarius makarius at sketis.net
Fri Sep 10 16:20:36 CEST 2010

* Parallel and asynchronous execution requires special care concerning
interrupts.  Structure Exn provides some convenience functions that
avoid working directly with raw Interrupt.  User code must not absorb
interrupts -- intermediate handling (for cleanup etc.) needs to be
followed by re-raising of the original exception.  Another common
source of mistakes are "handle _" patterns, which make the meaning of
the program subject to physical effects of the environment.

(Strictly speaking the only new thing is the extension of structure Exn.)


More information about the isabelle-dev mailing list