2011-08-23 wenzelm 2011-08-23 propagate editor perspective through document model;
2011-08-22 wenzelm 2011-08-22 some support for editor perspective;
2011-08-22 wenzelm 2011-08-22 discontinued redundant Edit_Command_ID;
2011-08-22 wenzelm 2011-08-22 reduced warnings;
2011-08-22 wenzelm 2011-08-22 tuned message;
2011-08-22 wenzelm 2011-08-22 old-style numbered structure index is legacy feature (hardly ever used now);
2011-08-22 wenzelm 2011-08-22 added official Text.Range.Ordering; some support for text perspective;
2011-08-22 wenzelm 2011-08-22 tuned signature;
2011-08-22 wenzelm 2011-08-22 reverted some odd changes to HOL/Import (cf. 74c08021ab2e);
2011-08-22 krauss 2011-08-22 merged
2011-08-21 krauss 2011-08-21 modernized specifications
2011-08-21 krauss 2011-08-21 removed session HOL/Subst -- now subsumed my more modern HOL/ex/Unification.thy
2011-08-21 krauss 2011-08-21 removed technical or trivial unused facts
2011-08-21 krauss 2011-08-21 more precise authors and comments; tuned order and headers
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