2011-08-22 blanchet 2011-08-22 tuning, plus started implementing tag equation generation for existential variables
2011-08-22 blanchet 2011-08-22 precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
2011-08-22 blanchet 2011-08-22 clearer terminology
2011-08-22 blanchet 2011-08-22 renamed "heavy" to "uniform", based on discussion with Nick Smallbone
2011-08-22 blanchet 2011-08-22 removed unused configuration option
2011-08-22 blanchet 2011-08-22 added caching for (in)finiteness checks
2011-08-22 blanchet 2011-08-22 remove needless typing information
2011-08-22 blanchet 2011-08-22 cleaner handling of polymorphic monotonicity inference
2011-08-22 blanchet 2011-08-22 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
2011-08-22 blanchet 2011-08-22 more precise warning
2011-08-22 blanchet 2011-08-22 added option to control soundness of encodings more precisely, for evaluation purposes
2011-08-22 blanchet 2011-08-22 make sound mode more sound (and clean up code)
2011-08-22 blanchet 2011-08-22 reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
2011-08-22 blanchet 2011-08-22 gracefully handle empty SPASS problems
2011-08-22 blanchet 2011-08-22 pass sound option to Sledgehammer tactic
2011-08-23 wenzelm 2011-08-23 tuned signature -- contrast physical output primitives versus Output.raw_message;
2011-08-23 wenzelm 2011-08-23 tuned signature;
2011-08-23 wenzelm 2011-08-23 discontinued slightly odd Future/Lazy.get_finished, which do not really fit into the execution model of Future.cancel/join_tasks (canceled tasks need to be dequeued and terminated explicitly);
2011-08-23 wenzelm 2011-08-23 some support for toplevel printing wrt. editor perspective (still inactive);
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