remove unused lemmas

fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas

remove some redundant simp rules

maintain recent future proofs at transaction boundaries;

incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof -- avoid full graph traversal of former Proofterm.join_bodies;

tuned;

tuned signature (again); tuned;

tuned signature -- treat structure Task_Queue as private to implementation;

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;

merged

remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas

merged

merged

avoid duplicated simp add option

observe distinction between sets and predicates more properly