NEWS
Mon, 05 Dec 2011 12:36:03 +0100 bulwahn NEWS
Sun, 04 Dec 2011 13:10:19 +0100 huffman remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
Thu, 01 Dec 2011 13:34:14 +0100 blanchet added "minimize" option for more control over automatic minimization
Thu, 01 Dec 2011 13:34:13 +0100 blanchet renamed "slicing" to "slice"
Thu, 01 Dec 2011 12:25:27 +0100 wenzelm renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Mon, 21 Nov 2011 23:29:53 +0100 wenzelm NEWS;
Sun, 20 Nov 2011 17:44:41 +0100 wenzelm 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
Sat, 19 Nov 2011 21:23:16 +0100 wenzelm NEWS;
Sat, 19 Nov 2011 21:18:38 +0100 wenzelm added ML antiquotation @{attributes};
Thu, 17 Nov 2011 15:07:46 +0100 huffman HOL-Word: removed more duplicate theorems
Thu, 17 Nov 2011 14:52:05 +0100 huffman HOL-Word: removed many duplicate theorems (see NEWS)
Wed, 16 Nov 2011 10:34:08 +0100 blanchet document "lam_trans" option
Wed, 09 Nov 2011 17:57:42 +0100 wenzelm sort assignment before simultaneous term_check, not isolated parse_term;
Mon, 07 Nov 2011 22:22:01 +0100 blanchet avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
Mon, 07 Nov 2011 14:23:50 +0100 wenzelm clarified attribute "mono_set": pure declaration, proper export in ML;
Mon, 07 Nov 2011 14:14:20 +0100 wenzelm misc tuning;
Sat, 29 Oct 2011 12:57:43 +0200 wenzelm uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
Fri, 28 Oct 2011 23:16:50 +0200 wenzelm refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
Fri, 21 Oct 2011 11:17:16 +0200 bulwahn NEWS
Wed, 19 Oct 2011 22:54:26 +0200 haftmann NEWS
Wed, 19 Oct 2011 15:42:43 +0200 wenzelm inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
Wed, 19 Oct 2011 09:11:21 +0200 bulwahn NEWS
Mon, 17 Oct 2011 14:22:14 +0200 noschinl (old) NEWS
Fri, 14 Oct 2011 18:55:29 +0200 haftmann NEWS
Thu, 13 Oct 2011 11:45:33 +0200 wenzelm discontinued obsolete 'types' command;
Wed, 12 Oct 2011 16:21:07 +0200 wenzelm discontinued obsolete alias structure ProofContext;
Sun, 09 Oct 2011 11:13:53 +0200 huffman Int.thy: discontinued some legacy theorems
Mon, 26 Sep 2011 21:13:26 +0200 wenzelm back to post-release mode;
Mon, 26 Sep 2011 21:09:28 +0200 wenzelm tuned;
Mon, 26 Sep 2011 20:53:53 +0200 wenzelm misc tuning for release;
Thu, 22 Sep 2011 14:12:16 -0700 huffman discontinued legacy theorem names from RealDef.thy
Thu, 22 Sep 2011 12:55:19 -0700 huffman discontinued HOLCF legacy theorem names
Thu, 22 Sep 2011 10:02:16 -0400 hoelzl NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
Wed, 21 Sep 2011 00:12:36 +0200 nipkow merged
Tue, 20 Sep 2011 05:47:11 +0200 nipkow New proof method "induction" that gives induction hypotheses the name IH.
Tue, 20 Sep 2011 22:11:22 +0200 haftmann official status for UN_singleton
Sun, 18 Sep 2011 15:57:36 +0200 wenzelm tuned;
Sun, 18 Sep 2011 15:39:55 +0200 wenzelm separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
Sun, 18 Sep 2011 14:48:25 +0200 wenzelm some tuning and re-ordering for release;
Sun, 18 Sep 2011 14:34:24 +0200 wenzelm misc tuning for release;
Thu, 15 Sep 2011 12:40:08 -0400 hoelzl removed further legacy rules from Complete_Lattices
Thu, 15 Sep 2011 17:06:00 +0200 noschinl NEWS on Complete_Lattices, Lattices
Tue, 13 Sep 2011 09:56:38 +0200 bulwahn correcting NEWS
Mon, 12 Sep 2011 13:19:10 -0700 huffman NEWS and CONTRIBUTORS
Mon, 12 Sep 2011 11:54:20 -0700 huffman remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
Mon, 12 Sep 2011 10:28:45 -0700 huffman fix typos
Mon, 12 Sep 2011 09:37:49 -0700 huffman NEWS for euclidean_space class
Mon, 12 Sep 2011 09:57:33 -0400 hoelzl adding NEWS and CONTRIBUTORS
Mon, 12 Sep 2011 13:35:35 +0200 bulwahn merged
Mon, 12 Sep 2011 10:27:36 +0200 bulwahn adding NEWS and CONTRIBUTORS
Mon, 12 Sep 2011 09:45:53 +0200 bulwahn tuned some symbol that probably went there by some strange encoding issue
Mon, 12 Sep 2011 11:05:32 +0200 blanchet added my contributions to NEWS and CONTRIBUTORS
Mon, 12 Sep 2011 09:07:23 +0200 nipkow NEWS fastsimp -> fastforce
Sun, 11 Sep 2011 13:49:42 -0700 huffman NEWS for Library/Product_Lattice.thy
Fri, 09 Sep 2011 00:22:18 +0200 krauss added syntactic classes for "inf" and "sup"
Wed, 07 Sep 2011 19:24:28 -0700 huffman merged
Wed, 07 Sep 2011 09:45:39 -0700 huffman remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
Thu, 08 Sep 2011 00:23:23 +0200 wenzelm merged
less more (0) -1000 -300 -100 -60 tip