summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip

remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead

rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy

add lemma power2_eq_iff

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