refined Future.cancel: explicit future allows to join actual cancellation; Document.cancel_execution: join nested future groups as well;

Future.promise: explicit abort operation (like uninterruptible future job); explicit cancel_scala message -- still unused;

editable raw text areas: allow user to clear content;

more robust use of set_exn_serial, which is based on PolyML.raiseWithLocation internally;

more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;

clarified Future.cond_forks: more uniform handling of exceptional situations;

Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.

merged

define complex exponential 'expi' as abbreviation for 'exp'

remove more bounded_linear locale interpretations (cf. f0de18b62d63)

optimize some proofs

add Multivariate_Analysis dependencies

import Library/Sum_of_Squares instead of reloading positivstellensatz.ML

declare euclidean_component_zero[simp] at the point it is proved

Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.

merged;