NEWS
2011-10-29 wenzelm 2011-10-29 uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
2011-10-28 wenzelm 2011-10-28 refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
2011-10-21 bulwahn 2011-10-21 NEWS
2011-10-19 haftmann 2011-10-19 NEWS
2011-10-19 wenzelm 2011-10-19 inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
2011-10-19 bulwahn 2011-10-19 NEWS
2011-10-17 noschinl 2011-10-17 (old) NEWS
2011-10-14 haftmann 2011-10-14 NEWS
2011-10-13 wenzelm 2011-10-13 discontinued obsolete 'types' command;
2011-10-12 wenzelm 2011-10-12 discontinued obsolete alias structure ProofContext;
2011-10-09 huffman 2011-10-09 Int.thy: discontinued some legacy theorems
2011-09-26 wenzelm 2011-09-26 back to post-release mode;
2011-09-26 wenzelm 2011-09-26 tuned;
2011-09-26 wenzelm 2011-09-26 misc tuning for release;
2011-09-22 huffman 2011-09-22 discontinued legacy theorem names from RealDef.thy
2011-09-22 huffman 2011-09-22 discontinued HOLCF legacy theorem names
2011-09-22 hoelzl 2011-09-22 NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
2011-09-21 nipkow 2011-09-21 merged
2011-09-20 nipkow 2011-09-20 New proof method "induction" that gives induction hypotheses the name IH.
2011-09-20 haftmann 2011-09-20 official status for UN_singleton
2011-09-18 wenzelm 2011-09-18 tuned;
2011-09-18 wenzelm 2011-09-18 separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
2011-09-18 wenzelm 2011-09-18 some tuning and re-ordering for release;
2011-09-18 wenzelm 2011-09-18 misc tuning for release;
2011-09-15 hoelzl 2011-09-15 removed further legacy rules from Complete_Lattices
2011-09-15 noschinl 2011-09-15 NEWS on Complete_Lattices, Lattices
2011-09-13 bulwahn 2011-09-13 correcting NEWS
2011-09-12 huffman 2011-09-12 NEWS and CONTRIBUTORS
2011-09-12 huffman 2011-09-12 remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
2011-09-12 huffman 2011-09-12 fix typos
2011-09-12 huffman 2011-09-12 NEWS for euclidean_space class
2011-09-12 hoelzl 2011-09-12 adding NEWS and CONTRIBUTORS
2011-09-12 bulwahn 2011-09-12 merged
2011-09-12 bulwahn 2011-09-12 adding NEWS and CONTRIBUTORS
2011-09-12 bulwahn 2011-09-12 tuned some symbol that probably went there by some strange encoding issue
2011-09-12 blanchet 2011-09-12 added my contributions to NEWS and CONTRIBUTORS
2011-09-12 nipkow 2011-09-12 NEWS fastsimp -> fastforce
2011-09-11 huffman 2011-09-11 NEWS for Library/Product_Lattice.thy
2011-09-09 krauss 2011-09-09 added syntactic classes for "inf" and "sup"
2011-09-07 huffman 2011-09-07 merged
2011-09-07 huffman 2011-09-07 remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
2011-09-08 wenzelm 2011-09-08 merged
2011-09-07 haftmann 2011-09-07 theory of saturated naturals contributed by Peter Gammie
2011-09-07 wenzelm 2011-09-07 NEWS on IsabelleText font;
2011-09-07 wenzelm 2011-09-07 some updates for release;
2011-09-07 wenzelm 2011-09-07 some tuning for release;
2011-09-07 wenzelm 2011-09-07 more NEWS;
2011-09-06 wenzelm 2011-09-06 some Isabelle/jEdit NEWS;
2011-09-06 huffman 2011-09-06 remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-09-06 huffman 2011-09-06 remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
2011-09-04 huffman 2011-09-04 remove redundant lemmas expi_add and expi_zero
2011-09-04 huffman 2011-09-04 remove redundant lemmas about LIMSEQ
2011-09-03 huffman 2011-09-03 remove duplicate lemma finite_choice in favor of finite_set_choice
2011-09-02 huffman 2011-09-02 remove redundant lemma reals_complete2 in favor of complete_real
2011-09-02 huffman 2011-09-02 remove more duplicate lemmas
2011-09-01 huffman 2011-09-01 simplify some proofs about uniform continuity, and add some new ones; rename some theorems according to standard naming scheme;
2011-09-01 huffman 2011-09-01 modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;
2011-08-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-26 huffman 2011-08-26 NEWS entry for setsum_norm ~> norm_setsum
2011-08-25 huffman 2011-08-25 replace some continuous_on lemmas with more general versions