2011-08-21 krauss 2011-08-21 added proof of idempotence, roughly after HOL/Subst/Unify.thy
2011-08-21 krauss 2011-08-21 tuned proofs, sledgehammering overly verbose parts
2011-08-21 krauss 2011-08-21 tuned notation
2011-08-21 krauss 2011-08-21 ported some lemmas from HOL/Subst/*; tuned order
2011-08-21 krauss 2011-08-21 changed constant names and notation to match HOL/Subst/*.thy, from which this theory is a clone.
2011-08-21 huffman 2011-08-21 merged
2011-08-21 huffman 2011-08-21 add lemmas interior_Times and closure_Times
2011-08-21 haftmann 2011-08-21 avoid pred/set mixture
2011-08-21 haftmann 2011-08-21 avoid pred/set mixture
2011-08-21 wenzelm 2011-08-21 merged
2011-08-21 huffman 2011-08-21 remove unnecessary euclidean_space class constraints
2011-08-21 huffman 2011-08-21 section -> subsection
2011-08-21 huffman 2011-08-21 scale dependency graph to fit on page
2011-08-21 wenzelm 2011-08-21 more robust initialization of token marker and line context wrt. session startup;
2011-08-21 wenzelm 2011-08-21 tuned Parse.group: delayed failure message;
2011-08-21 wenzelm 2011-08-21 avoid actual Color.white, which would be turned into Color.black by org.gjt.sp.jedit.print.BufferPrintable;
2011-08-21 wenzelm 2011-08-21 default style for user fonts -- to prevent org.gjt.sp.jedit.print.BufferPrintable from choking on null;
2011-08-21 wenzelm 2011-08-21 tuned;
2011-08-21 wenzelm 2011-08-21 discontinued somewhat pointless Par_List.map_name -- most of the time is spent in tokenization;
2011-08-21 wenzelm 2011-08-21 discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;
2011-08-21 wenzelm 2011-08-21 merged
2011-08-20 huffman 2011-08-20 replace lemma realpow_two_diff with new lemma square_diff_square_factored
2011-08-20 huffman 2011-08-20 remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
2011-08-20 huffman 2011-08-20 move lemma add_eq_0_iff to Groups.thy
2011-08-20 huffman 2011-08-20 remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead
2011-08-20 huffman 2011-08-20 rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
2011-08-20 huffman 2011-08-20 add lemma power2_eq_iff
2011-08-20 huffman 2011-08-20 remove some over-specific rules from the simpset
2011-08-20 huffman 2011-08-20 merged
2011-08-20 huffman 2011-08-20 redefine constant 'trivial_limit' as an abbreviation
2011-08-21 wenzelm 2011-08-21 purely functional task_queue.ML -- moved actual interrupt_unsynchronized to future.ML;
2011-08-21 wenzelm 2011-08-21 refined Task_Queue.cancel: passive tasks are considered running due to pending abort operation;
2011-08-20 wenzelm 2011-08-20 odd workaround for odd problem of load order in HOL/ex/ROOT.ML (!??);
2011-08-20 wenzelm 2011-08-20 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-08-20 wenzelm 2011-08-20 clarified get_imports -- should not rely on accidental order within graph;
2011-08-20 wenzelm 2011-08-20 tuned Table.delete_safe: avoid potentially expensive attempt of delete;
2011-08-20 wenzelm 2011-08-20 discontinued "Interrupt", which could disturb administrative tasks of the document model;
2011-08-20 wenzelm 2011-08-20 more direct balanced version Ord_List.unions;
2011-08-20 wenzelm 2011-08-20 reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
2011-08-20 wenzelm 2011-08-20 tuned future priorities (again);
2011-08-20 wenzelm 2011-08-20 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;
2011-08-20 wenzelm 2011-08-20 added Future.joins convenience; clarified Future.map: based on Future.cond_forks;
2011-08-20 haftmann 2011-08-20 merged
2011-08-20 haftmann 2011-08-20 deactivated »unknown« nitpick example
2011-08-20 haftmann 2011-08-20 merged
2011-08-20 haftmann 2011-08-20 tuned proof
2011-08-20 haftmann 2011-08-20 more uniform formatting of specifications
2011-08-20 haftmann 2011-08-20 compatibility layer
2011-08-20 haftmann 2011-08-20 merged
2011-08-19 haftmann 2011-08-19 more concise definition for Inf, Sup on bool
2011-08-18 noschinl 2011-08-18 do not call ghc with -fglasgow-exts
2011-08-19 huffman 2011-08-19 remove some redundant simp rules about sqrt
2011-08-19 huffman 2011-08-19 move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
2011-08-19 huffman 2011-08-19 remove unused lemma DERIV_sin_add
2011-08-19 huffman 2011-08-19 remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
2011-08-19 huffman 2011-08-19 remove redundant lemma exp_ln_eq in favor of ln_unique
2011-08-19 huffman 2011-08-19 merged
2011-08-19 huffman 2011-08-19 Lim.thy: legacy theorems
2011-08-19 huffman 2011-08-19 SEQ.thy: legacy theorem names
2011-08-19 huffman 2011-08-19 delete unused lemmas about limits