ML

• Proper interrupts (e.g. timeouts) are now distinguished from Poly/ML runtime system breakdown, using Exn.Interrupt_Breakdown as quasi-error. Exn.is_interrupt covers all kinds of interrupts as before, but Exn.is_interrupt_proper and Exn.is_interrupt_breakdown are more specific. Subtle INCOMPATIBILITY in the semantics of ML evaluation.

This refers to Isabelle/280a228dc2f1.