2011-08-23 wenzelm 2011-08-23 fixed document;
2011-08-23 wenzelm 2011-08-23 tuned signature;
2011-08-23 wenzelm 2011-08-23 merged
2011-08-23 blanchet 2011-08-23 always use TFF if possible
2011-08-23 blanchet 2011-08-23 clearer separator in generated file names
2011-08-23 blanchet 2011-08-23 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
2011-08-23 blanchet 2011-08-23 updated known failures for Z3 3.0 TPTP
2011-08-23 blanchet 2011-08-23 updated Z3 docs
2011-08-23 blanchet 2011-08-23 avoid TFF format with older Vampire versions
2011-08-23 blanchet 2011-08-23 update the Vampire related parts of the documentation
2011-08-23 blanchet 2011-08-23 fixed TFF slicing
2011-08-23 blanchet 2011-08-23 kindly ask Vampire to output axiom names
2011-08-23 blanchet 2011-08-23 added formats to the slice and use TFF for remote Vampire
2011-08-23 haftmann 2011-08-23 tuned specifications, syntax and proofs
2011-08-22 haftmann 2011-08-22 tuned specifications and syntax
2011-08-23 Cezary Kaliszyk 2011-08-23 Quotient Package: some infrastructure for lifting inside sets
2011-08-22 blanchet 2011-08-22 include all encodings in tests, now that the incompleteness of some encodings has been addressed
2011-08-22 blanchet 2011-08-22 change Metis's default settings if type information axioms are generated
2011-08-22 blanchet 2011-08-22 we must tag any type whose ground types intersect a nonmonotonic type
2011-08-22 blanchet 2011-08-22 prefer the lighter, slightly unsound monotonicity-based encodings for Metis
2011-08-22 blanchet 2011-08-22 made reconstruction of type tag equalities "\?x = \?x" reliable
2011-08-22 blanchet 2011-08-22 tuning ATP problem output
2011-08-22 blanchet 2011-08-22 revert guard logic -- make sure that typing information is generated for existentials
2011-08-22 blanchet 2011-08-22 generate tag equations for existential variables
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