Fri, 20 Apr 2012 11:14:39 +0200 hoelzl hide code generation facts in the Float theory, they are only exported for Approximation
Fri, 20 Apr 2012 10:47:04 +0200 nipkow merged
Fri, 20 Apr 2012 10:46:55 +0200 nipkow forgot to add file
Fri, 20 Apr 2012 10:18:08 +0200 huffman make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
Thu, 19 Apr 2012 23:18:47 +0200 wenzelm merged
Thu, 19 Apr 2012 22:21:15 +0200 hoelzl NEWS
Thu, 19 Apr 2012 22:13:46 +0200 hoelzl transfer now handles Let
Thu, 19 Apr 2012 20:19:24 +0200 nipkow merged
Thu, 19 Apr 2012 20:19:13 +0200 nipkow added revised version of Abs_Int
Thu, 19 Apr 2012 19:36:09 +0200 huffman add transfer rule for Let
Thu, 19 Apr 2012 19:32:30 +0200 huffman add code lemmas for word operations
Thu, 19 Apr 2012 19:18:47 +0200 haftmann tuned whitespace
Thu, 19 Apr 2012 19:18:11 +0200 haftmann dropped dead code
Thu, 19 Apr 2012 18:24:40 +0200 kuncar rename no_code to no_abs_code - more appropriate name
Thu, 19 Apr 2012 17:31:34 +0200 kuncar use tnames for bound variables in rsp thms
Thu, 19 Apr 2012 17:49:08 +0200 blanchet true delayed evaluation of "SPASS_VERSION" environment variable
Thu, 19 Apr 2012 17:49:02 +0200 blanchet merged
Thu, 19 Apr 2012 11:14:57 +0200 blanchet use latest Z3
Thu, 19 Apr 2012 17:32:35 +0200 nipkow merged
Thu, 19 Apr 2012 17:32:30 +0200 nipkow reorganised IMP
Thu, 19 Apr 2012 11:55:30 +0200 hoelzl use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
Wed, 18 Apr 2012 14:29:22 +0200 hoelzl use lifting to introduce floating point numbers
Wed, 18 Apr 2012 14:29:21 +0200 hoelzl replace the float datatype by a type with unique representation
Wed, 18 Apr 2012 14:29:20 +0200 hoelzl add lemmas to remove real conversions when compared to power of numerals
Wed, 18 Apr 2012 14:29:20 +0200 hoelzl add simp rules to rewrite comparisons of 1 and real
Wed, 18 Apr 2012 14:29:19 +0200 hoelzl add lemma to equate floor and div
Wed, 18 Apr 2012 14:29:18 +0200 hoelzl add powr_inj
Wed, 18 Apr 2012 14:29:17 +0200 hoelzl add lemmas to rewrite powr to power
Wed, 18 Apr 2012 14:29:16 +0200 hoelzl add lemmas to compare log with 0 and 1
Wed, 18 Apr 2012 14:29:05 +0200 hoelzl add ceiling_diff_floor_le_1
Thu, 19 Apr 2012 23:15:58 +0200 wenzelm display Java 7 only code for now (cf. b9e2ed4b1579);
Thu, 19 Apr 2012 21:53:24 +0200 wenzelm some sidekick options for more advanced completion;
Thu, 19 Apr 2012 21:47:50 +0200 wenzelm custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
Thu, 19 Apr 2012 21:42:24 +0200 wenzelm tuned imports;
Thu, 19 Apr 2012 19:54:48 +0200 wenzelm more robust wrt. exceptions;
Thu, 19 Apr 2012 15:47:32 +0200 wenzelm accomodate digits within Isar command names, notably 'try0';
Thu, 19 Apr 2012 15:02:13 +0200 wenzelm more robust Sledgehammer in Prover IDE;
Thu, 19 Apr 2012 14:59:17 +0200 wenzelm test with jdk-7u3 that is also bundled;
Thu, 19 Apr 2012 12:28:10 +0200 kuncar create thm names correctly
Thu, 19 Apr 2012 13:19:57 +0200 wenzelm updated components according to tentative bundle;
Thu, 19 Apr 2012 13:15:06 +0200 wenzelm back to isatest with official polyml-5.4.1 (cf. ffa6e10df091);
Thu, 19 Apr 2012 11:52:07 +0200 huffman use simpler method for preserving bound variable names in transfer tactic
Thu, 19 Apr 2012 10:49:47 +0200 huffman tuned lemmas (v)image_id;
Thu, 19 Apr 2012 11:10:03 +0200 blanchet use latest SPASS
Thu, 19 Apr 2012 11:00:12 +0200 blanchet doc update
Thu, 19 Apr 2012 10:16:51 +0200 haftmann dropped dead code;
Thu, 19 Apr 2012 08:45:13 +0200 huffman generate abs_induct rules for quotient types
Thu, 19 Apr 2012 09:58:54 +0200 haftmann tuned
Thu, 19 Apr 2012 09:45:49 +0200 haftmann corrected Nbe.static_value: ignore cached compilations;
Thu, 19 Apr 2012 09:31:36 +0200 haftmann tuned heading
Wed, 18 Apr 2012 21:47:26 +0200 haftmann tuned name
Thu, 19 Apr 2012 07:25:44 +0100 sultana improved threading of thy-values through interpret functions;
Thu, 19 Apr 2012 07:25:41 +0100 sultana exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
Wed, 18 Apr 2012 17:44:39 +0200 huffman add option to transfer method for specifying variables not to generalize over
Tue, 17 Apr 2012 16:21:47 +1000 Thomas Sewell New tactic "word_bitwise" expands word equalities/inequalities into logic.
Wed, 18 Apr 2012 23:57:44 +0200 kuncar setup_lifting: no_code switch and supoport for quotient theorems
Wed, 18 Apr 2012 23:13:11 +0200 blanchet remove old TPTP CNF/FOF parser; always use Nik's new parser
Wed, 18 Apr 2012 23:13:10 +0200 blanchet more standard SZS output
Wed, 18 Apr 2012 22:40:25 +0200 blanchet Sledgehammer NEWS and CONTRIBUTORS
Wed, 18 Apr 2012 22:40:25 +0200 blanchet tuned SZS status output
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip