remove some over-specific rules from the simpset

merged

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

Lim.thy: legacy theorems

SEQ.thy: legacy theorem names

delete unused lemmas about limits

Transcendental.thy: add tendsto_intros lemmas; new isCont theorems; simplify some proofs.

add lemma isCont_tendsto_compose

merged

Transcendental.thy: remove several unused lemmas and simplify some proofs

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

moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace

avoid case-sensitive name for example theory

merged

case_names NEWS

adding documentation about simps equation in the inductive package

activating narrowing-based quickcheck by default

more precise treatment of exception nesting and serial numbers;

more careful treatment of exception serial numbers, with propagation to message channel;

updated sequential version (cf. b94951f06e48);

tuned comments;

tuned document; tuned proofs;

clarified Par_Exn.release_first: prefer plain exn, before falling back on full pack of parallel exceptions;

export Par_List.managed_results, to enable specific treatment of results apart from default Par_Exn.release_first;

tune Par_Exn.make: balance merge; clarified Par_Exn.dest: later exceptions first;

Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.

merged

HOL-IMP: respect set/pred distinction

Determinants.thy: avoid using mem_def/Collect_def

Wfrec.thy: respect set/pred distinction

follow updates of Isabelle/Pure;

merged

IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library

merged

Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems

add lemma tendsto_compose_eventually; use it to shorten some proofs

Topology_Euclidean_Space.thy: simplify some proofs

add lemma metric_tendsto_imp_tendsto

simplify proofs of lemmas open_interval, closed_interval

identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;

clarified Par_Exn.release_first: traverse topmost list structure only, not arbitrary depths of nested Par_Exn;

more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;

tuned signature;

merged

merged

merged

avoid Collect_def in proof

modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;

improved default context for ML toplevel pretty-printing;

less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);

some convenience actions/shortcuts for control symbols;

export Function_Fun.fun_config for user convenience;

moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);

distinguish THF syntax with and without choice (Satallax vs. LEO-II)

merged

add simp rules for isCont

updated keywords -- old codegen is no longer in Pure;

include HOL-Library keywords for the sake of recdef;

merged

Multivariate_Analysis includes Determinants.thy, but doesn't import it by default

get Multivariate_Analysis/Determinants.thy compiled and working again

get Library/Permutations.thy compiled and working again

workaround for Cygwin, to make it work in the important special case without extra files;

more robust Thy_Header.base_name, with minimal assumptions about path syntax; Isabelle.buffer_path: keep platform syntax;