NEWS
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
Wed, 07 Sep 2011 23:38:52 +0200 haftmann theory of saturated naturals contributed by Peter Gammie
Wed, 07 Sep 2011 21:10:47 +0200 wenzelm NEWS on IsabelleText font;
Wed, 07 Sep 2011 20:49:45 +0200 wenzelm some updates for release;
Wed, 07 Sep 2011 20:29:54 +0200 wenzelm some tuning for release;
Wed, 07 Sep 2011 11:26:27 +0200 wenzelm more NEWS;
Tue, 06 Sep 2011 21:56:11 +0200 wenzelm some Isabelle/jEdit NEWS;
Tue, 06 Sep 2011 07:48:59 -0700 huffman remove redundant lemma real_sum_squared_expand in favor of power2_sum
Tue, 06 Sep 2011 07:45:18 -0700 huffman remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
Sun, 04 Sep 2011 10:05:52 -0700 huffman remove redundant lemmas expi_add and expi_zero
Sun, 04 Sep 2011 09:49:45 -0700 huffman remove redundant lemmas about LIMSEQ
Sat, 03 Sep 2011 09:26:11 -0700 huffman remove duplicate lemma finite_choice in favor of finite_set_choice
Fri, 02 Sep 2011 16:48:30 -0700 huffman remove redundant lemma reals_complete2 in favor of complete_real
Fri, 02 Sep 2011 13:57:12 -0700 huffman remove more duplicate lemmas
Thu, 01 Sep 2011 10:41:19 -0700 huffman simplify some proofs about uniform continuity, and add some new ones;
Thu, 01 Sep 2011 09:02:14 -0700 huffman modernize lemmas about 'continuous' and 'continuous_on';
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Fri, 26 Aug 2011 15:11:26 -0700 huffman NEWS entry for setsum_norm ~> norm_setsum
Thu, 25 Aug 2011 19:41:38 -0700 huffman replace some continuous_on lemmas with more general versions
Thu, 25 Aug 2011 16:50:55 -0700 huffman remove legacy theorem Lim_inner
Thu, 25 Aug 2011 15:35:54 -0700 huffman remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
Thu, 25 Aug 2011 12:43:55 -0700 huffman rename subset_{interior,closure} to {interior,closure}_mono;
Fri, 19 Aug 2011 19:33:31 +0200 haftmann more concise definition for Inf, Sup on bool
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Thu, 18 Aug 2011 17:42:18 +0200 nipkow case_names NEWS
Wed, 10 Aug 2011 13:13:37 -0700 huffman more uniform naming scheme for finite cartesian product type and related theorems
Tue, 09 Aug 2011 08:06:15 +0200 haftmann more uniform naming scheme for Inf/INF and Sup/SUP lemmas
Tue, 09 Aug 2011 07:44:17 +0200 haftmann merged
Mon, 08 Aug 2011 19:21:11 +0200 haftmann dropped lemmas (Inf|Sup)_(singleton|binary)
Mon, 08 Aug 2011 19:26:53 -0700 huffman rename type 'a net to 'a filter, following standard mathematical terminology
Thu, 04 Aug 2011 07:31:43 +0200 haftmann NEWS
Wed, 03 Aug 2011 16:08:02 +0200 bulwahn NEWS
Tue, 02 Aug 2011 08:28:34 -0700 huffman Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
less more (0) -1000 -300 -100 -60 tip