tuned;

clarified signature;

more robust management of resources, using Thread_Attributes.uninterruptible;

tuned;

tuned;

tuned signature;

clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);

clarified signature;

clarified modules;

unused;

clarified order of modules: early access to interrupt management of Isabelle_Threads;

tuned: prefer antiquotation for try-catch;

tuned: prefer antiquotation for try-catch;

tuned: prefer antiquotation for try-finally;

omit pointless capture/release (see also 469a375212c1);

omit pointless capture/release (see also 26774ccb1c74);

clarified signature: avoid association with potentially dangerous Exn.capture;

more robust: catch/finally part is uninterruptible;

more position information, e.g. for warning about fn-pattern;

unused;

more general ML_Antiquotation.special_form; more general "try" forms: support 'finally' or 'catch';

Importing or moving a few more useful theorems

merged

A few new theorems

avoid legacy binding errors in Sledgehammer Isar proofs

parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition

added argo

allow (~) syntax in TPTP proofs for unapplied negation

reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs

use same associativity as Isabelle when parsing HOL proofs

improved Sledgehammer's HOL proof parser w.r.t. negation

clarified signature;