Changes

Summary

1. moved variable bindings to tighter scope
2. removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer
3. removed unused function parameter
4. merged
5. A couple of new lemmas
6. merged
7. more NEWS;
8. explicitly reject 'handle' with catch-all patterns;
9. avoid accidental 'handle' of interrupts;
10. tuned: prefer try-catch/finally over low-level 'handle';
11. clarified treatment of exceptions: avoid catch-all handlers;
12. clarified output vs. error: presence of error messages means error (see also cb7264721c91);
13. tuned;
14. more robust management of resources, using Thread_Attributes.uninterruptible;
15. tuned;
16. clarified signature;
17. more robust management of resources, using Thread_Attributes.uninterruptible;
18. tuned;
19. tuned;
20. tuned signature;
21. clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
22. clarified signature;
23. clarified modules;
24. unused;
25. clarified order of modules: early access to interrupt management of Isabelle_Threads;
26. tuned: prefer antiquotation for try-catch;
27. tuned: prefer antiquotation for try-catch;
28. tuned: prefer antiquotation for try-finally;
29. omit pointless capture/release (see also 469a375212c1);
30. omit pointless capture/release (see also 26774ccb1c74);
31. clarified signature: avoid association with potentially dangerous Exn.capture;
32. more robust: catch/finally part is uninterruptible;
33. more position information, e.g. for warning about fn-pattern;
34. unused;
35. more general ML_Antiquotation.special_form; more general "try" forms: support 'finally' or 'catch';