redefine constant 'trivial_limit' as an abbreviation

purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;

refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;

odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);

refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

clarified get_imports -- should not rely on accidental order within graph;

tuned Table.delete_safe: avoid potentially expensive attempt of delete;

discontinued "Interrupt", which could disturb administrative tasks of the document model;

more direct balanced version Ord_List.unions;

reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;

tuned future priorities (again);

clarified fulfill_norm_proof: no join_thms yet; clarified priority of fulfill_proof_future, which is followed by explicit join_thms; explicit Thm.future_body_of without join yet; tuned Thm.future_result: join_promises without fulfill_norm_proof;

added Future.joins convenience; clarified Future.map: based on Future.cond_forks;

merged

deactivated »unknown« nitpick example

merged

tuned proof

more uniform formatting of specifications

compatibility layer

merged

more concise definition for Inf, Sup on bool

do not call ghc with -fglasgow-exts

remove some redundant simp rules about sqrt

move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs

remove unused lemma DERIV_sin_add

remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong

remove redundant lemma exp_ln_eq in favor of ln_unique

merged