Fri, 20 Apr 2012 23:34:03 +0200 wenzelm merged
Fri, 20 Apr 2012 22:05:07 +0200 huffman add transfer rule for nat_case
Fri, 20 Apr 2012 22:54:13 +0200 huffman uniform naming scheme for transfer rules
Fri, 20 Apr 2012 22:49:40 +0200 huffman rename 'correspondence' method to 'transfer_prover'
Fri, 20 Apr 2012 18:29:21 +0200 kuncar hide the invariant constant for relators: invariant_commute infrastracture
Fri, 20 Apr 2012 23:16:46 +0200 wenzelm improved interleaving of start_execution vs. cancel_execution of the next update;
Fri, 20 Apr 2012 23:15:44 +0200 wenzelm tuned proofs;
Fri, 20 Apr 2012 22:48:48 +0200 wenzelm always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;
Fri, 20 Apr 2012 22:51:06 +0200 wenzelm tuned;
Fri, 20 Apr 2012 20:29:44 +0200 wenzelm simplified internal actor protocol;
Fri, 20 Apr 2012 20:21:22 +0200 wenzelm builtin timing for main operations;
Fri, 20 Apr 2012 15:49:45 +0200 huffman add secondary transfer rule for universal quantifiers on non-bi-total relations
Fri, 20 Apr 2012 15:34:33 +0200 huffman move definition of set_rel into Library/Quotient_Set.thy
Fri, 20 Apr 2012 15:30:13 +0200 huffman add transfer rule for 'id'
Fri, 20 Apr 2012 14:57:19 +0200 huffman add new transfer rules and setup for lifting package
Fri, 20 Apr 2012 10:37:00 +0200 huffman setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq
Fri, 20 Apr 2012 11:17:01 +0200 hoelzl NEWS
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;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip