Wed, 24 Aug 2011 13:37:43 +0200 wenzelm more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
Wed, 24 Aug 2011 13:03:39 +0200 wenzelm update_perspective without actual edits, bypassing the full state assignment protocol;
Tue, 23 Aug 2011 21:19:24 +0200 wenzelm tuned;
Tue, 23 Aug 2011 21:14:59 +0200 wenzelm handle potentially more approriate BufferUpdate.LOADED event;
Mon, 22 Aug 2011 23:39:05 +0200 wenzelm special treatment of structure index 1 in Pure, including legacy warning;
Tue, 23 Aug 2011 19:49:21 +0200 blanchet compile
Tue, 23 Aug 2011 19:00:48 +0200 blanchet added "max_calls" option to get a fixed number of Sledgehammer calls per theory
Tue, 23 Aug 2011 18:42:05 +0200 blanchet beef up "sledgehammer_tac" reconstructor
Tue, 23 Aug 2011 18:42:05 +0200 blanchet clean up Sledgehammer tactic
Tue, 23 Aug 2011 17:44:31 +0200 wenzelm fixed document;
Tue, 23 Aug 2011 17:43:06 +0200 wenzelm tuned signature;
Tue, 23 Aug 2011 17:12:54 +0200 wenzelm merged
Tue, 23 Aug 2011 16:37:23 +0200 blanchet always use TFF if possible
Tue, 23 Aug 2011 16:14:19 +0200 blanchet clearer separator in generated file names
Tue, 23 Aug 2011 16:07:01 +0200 blanchet exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
Tue, 23 Aug 2011 15:50:27 +0200 blanchet updated known failures for Z3 3.0 TPTP
Tue, 23 Aug 2011 15:18:46 +0200 blanchet updated Z3 docs
Tue, 23 Aug 2011 15:15:43 +0200 blanchet avoid TFF format with older Vampire versions
Tue, 23 Aug 2011 14:57:16 +0200 blanchet update the Vampire related parts of the documentation
Tue, 23 Aug 2011 14:44:19 +0200 blanchet fixed TFF slicing
Tue, 23 Aug 2011 14:44:19 +0200 blanchet kindly ask Vampire to output axiom names
Tue, 23 Aug 2011 14:44:19 +0200 blanchet added formats to the slice and use TFF for remote Vampire
Tue, 23 Aug 2011 07:14:09 +0200 haftmann tuned specifications, syntax and proofs
Mon, 22 Aug 2011 22:00:36 +0200 haftmann tuned specifications and syntax
Tue, 23 Aug 2011 03:34:17 +0900 Cezary Kaliszyk Quotient Package: some infrastructure for lifting inside sets
Mon, 22 Aug 2011 15:02:45 +0200 blanchet include all encodings in tests, now that the incompleteness of some encodings has been addressed
Mon, 22 Aug 2011 15:02:45 +0200 blanchet change Metis's default settings if type information axioms are generated
Mon, 22 Aug 2011 15:02:45 +0200 blanchet we must tag any type whose ground types intersect a nonmonotonic type
Mon, 22 Aug 2011 15:02:45 +0200 blanchet prefer the lighter, slightly unsound monotonicity-based encodings for Metis
Mon, 22 Aug 2011 15:02:45 +0200 blanchet made reconstruction of type tag equalities "\?x = \?x" reliable
Mon, 22 Aug 2011 15:02:45 +0200 blanchet tuning ATP problem output
Mon, 22 Aug 2011 15:02:45 +0200 blanchet revert guard logic -- make sure that typing information is generated for existentials
Mon, 22 Aug 2011 15:02:45 +0200 blanchet generate tag equations for existential variables
Mon, 22 Aug 2011 15:02:45 +0200 blanchet tuning, plus started implementing tag equation generation for existential variables
Mon, 22 Aug 2011 15:02:45 +0200 blanchet precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
Mon, 22 Aug 2011 15:02:45 +0200 blanchet clearer terminology
Mon, 22 Aug 2011 15:02:45 +0200 blanchet renamed "heavy" to "uniform", based on discussion with Nick Smallbone
Mon, 22 Aug 2011 15:02:45 +0200 blanchet removed unused configuration option
Mon, 22 Aug 2011 15:02:45 +0200 blanchet added caching for (in)finiteness checks
Mon, 22 Aug 2011 15:02:45 +0200 blanchet remove needless typing information
Mon, 22 Aug 2011 15:02:45 +0200 blanchet cleaner handling of polymorphic monotonicity inference
Mon, 22 Aug 2011 15:02:45 +0200 blanchet started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
Mon, 22 Aug 2011 15:02:45 +0200 blanchet more precise warning
Mon, 22 Aug 2011 15:02:45 +0200 blanchet added option to control soundness of encodings more precisely, for evaluation purposes
Mon, 22 Aug 2011 15:02:45 +0200 blanchet make sound mode more sound (and clean up code)
Mon, 22 Aug 2011 15:02:45 +0200 blanchet reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
Mon, 22 Aug 2011 15:02:45 +0200 blanchet gracefully handle empty SPASS problems
Mon, 22 Aug 2011 15:02:45 +0200 blanchet pass sound option to Sledgehammer tactic
Tue, 23 Aug 2011 16:53:05 +0200 wenzelm tuned signature -- contrast physical output primitives versus Output.raw_message;
Tue, 23 Aug 2011 16:41:16 +0200 wenzelm tuned signature;
Tue, 23 Aug 2011 16:39:21 +0200 wenzelm 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);
Tue, 23 Aug 2011 15:48:41 +0200 wenzelm some support for toplevel printing wrt. editor perspective (still inactive);
Tue, 23 Aug 2011 12:20:12 +0200 wenzelm propagate editor perspective through document model;
Mon, 22 Aug 2011 21:42:02 +0200 wenzelm some support for editor perspective;
Mon, 22 Aug 2011 21:09:26 +0200 wenzelm discontinued redundant Edit_Command_ID;
Mon, 22 Aug 2011 20:11:44 +0200 wenzelm reduced warnings;
Mon, 22 Aug 2011 20:00:04 +0200 wenzelm tuned message;
Mon, 22 Aug 2011 17:10:22 +0200 wenzelm old-style numbered structure index is legacy feature (hardly ever used now);
Mon, 22 Aug 2011 16:12:23 +0200 wenzelm added official Text.Range.Ordering;
Mon, 22 Aug 2011 14:15:52 +0200 wenzelm tuned signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip