Thu, 25 Aug 2011 19:12:58 +0200 wenzelm tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
Thu, 25 Aug 2011 17:38:12 +0200 wenzelm maintain last_execs assignment on Scala side;
Thu, 25 Aug 2011 16:44:06 +0200 wenzelm propagate information about last command with exec state assignment through document model;
Thu, 25 Aug 2011 13:24:41 +0200 wenzelm tuned signature;
Thu, 25 Aug 2011 11:41:48 +0200 wenzelm slightly more abstract Command.Perspective;
Thu, 25 Aug 2011 11:27:37 +0200 wenzelm slightly more abstract Text.Perspective;
Wed, 24 Aug 2011 23:20:05 +0200 wenzelm tuned proofs;
Wed, 24 Aug 2011 23:19:40 +0200 wenzelm tuned syntax -- avoid ambiguities;
Wed, 24 Aug 2011 23:00:53 +0200 wenzelm more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
Wed, 24 Aug 2011 09:23:26 -0700 huffman delete commented-out dead code
Wed, 24 Aug 2011 09:08:07 -0700 huffman merged
Wed, 24 Aug 2011 09:08:00 -0700 huffman change some subsection headings to subsubsection
Tue, 23 Aug 2011 16:47:48 -0700 huffman remove unnecessary lemma card_ge1
Tue, 23 Aug 2011 16:17:22 -0700 huffman move connected_real_lemma to the one place it is used
Wed, 24 Aug 2011 17:30:25 +0200 wenzelm merged
Wed, 24 Aug 2011 15:25:39 +0200 blanchet make sure that all facts are passed to ATP from minimizer
Wed, 24 Aug 2011 11:17:33 +0200 blanchet more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
Wed, 24 Aug 2011 11:17:33 +0200 blanchet specify timeout for "sledgehammer_tac"
Wed, 24 Aug 2011 11:17:33 +0200 blanchet tuning
Wed, 24 Aug 2011 10:59:22 +0900 Cezary Kaliszyk Quotient Package: add mem_rsp, mem_prs, tune proofs.
Tue, 23 Aug 2011 15:46:53 -0700 huffman merged
Tue, 23 Aug 2011 14:11:02 -0700 huffman declare euclidean_simps [simp] at the point they are proved;
Tue, 23 Aug 2011 07:12:05 -0700 huffman merged
Mon, 22 Aug 2011 18:15:33 -0700 huffman merged
Mon, 22 Aug 2011 17:22:49 -0700 huffman avoid warnings
Mon, 22 Aug 2011 16:49:45 -0700 huffman comment out dead code to avoid compiler warnings
Mon, 22 Aug 2011 10:43:10 -0700 huffman legacy theorem names
Mon, 22 Aug 2011 10:19:39 -0700 huffman remove duplicate lemma
Tue, 23 Aug 2011 23:18:13 +0200 blanchet fixed "hBOOL" of existential variables, and generate more helpers
Tue, 23 Aug 2011 22:44:08 +0200 blanchet don't select facts when using sledgehammer_tac for reconstruction
Tue, 23 Aug 2011 20:35:41 +0200 blanchet don't perform a triviality check if the goal is skipped anyway
Tue, 23 Aug 2011 19:50:25 +0200 blanchet optional reconstructor
Wed, 24 Aug 2011 17:25:45 +0200 wenzelm misc tuning and simplification;
Wed, 24 Aug 2011 17:16:48 +0200 wenzelm tuned pri: prefer purging of canceled execution;
Wed, 24 Aug 2011 17:14:31 +0200 wenzelm tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
Wed, 24 Aug 2011 16:49:48 +0200 wenzelm clarified Document.Node.clear -- retain header (cf. ML version);
Wed, 24 Aug 2011 16:27:27 +0200 wenzelm clarified norm_header/header_edit -- disallow update of loaded theories;
Wed, 24 Aug 2011 15:55:43 +0200 wenzelm misc tuning and simplification;
Wed, 24 Aug 2011 15:30:43 +0200 wenzelm ignore irrelevant timings;
Wed, 24 Aug 2011 13:40:10 +0200 wenzelm print state only for visible command, to avoid wasting resources for the larger part of the text;
Wed, 24 Aug 2011 13:38:07 +0200 wenzelm early filtering of unchanged perspective;
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip