NEWS
2011-10-09 ago Int.thy: discontinued some legacy theorems
2011-09-26 ago back to post-release mode;
2011-09-26 ago tuned;
2011-09-26 ago misc tuning for release;
2011-09-22 ago discontinued legacy theorem names from RealDef.thy
2011-09-22 ago discontinued HOLCF legacy theorem names
2011-09-22 ago NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
2011-09-21 ago merged
2011-09-20 ago New proof method "induction" that gives induction hypotheses the name IH.
2011-09-20 ago official status for UN_singleton
2011-09-18 ago tuned;
2011-09-18 ago separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
2011-09-18 ago some tuning and re-ordering for release;
2011-09-18 ago misc tuning for release;
2011-09-15 ago removed further legacy rules from Complete_Lattices
2011-09-15 ago NEWS on Complete_Lattices, Lattices
2011-09-13 ago correcting NEWS
2011-09-12 ago NEWS and CONTRIBUTORS
2011-09-12 ago remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
2011-09-12 ago fix typos
2011-09-12 ago NEWS for euclidean_space class
2011-09-12 ago adding NEWS and CONTRIBUTORS
2011-09-12 ago merged
2011-09-12 ago adding NEWS and CONTRIBUTORS
2011-09-12 ago tuned some symbol that probably went there by some strange encoding issue
2011-09-12 ago added my contributions to NEWS and CONTRIBUTORS
2011-09-12 ago NEWS fastsimp -> fastforce
2011-09-11 ago NEWS for Library/Product_Lattice.thy
2011-09-09 ago added syntactic classes for "inf" and "sup"
2011-09-07 ago merged
2011-09-07 ago remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
2011-09-08 ago merged
2011-09-07 ago theory of saturated naturals contributed by Peter Gammie
2011-09-07 ago NEWS on IsabelleText font;
2011-09-07 ago some updates for release;
2011-09-07 ago some tuning for release;
2011-09-07 ago more NEWS;
2011-09-06 ago some Isabelle/jEdit NEWS;
2011-09-06 ago remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-09-06 ago remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
2011-09-04 ago remove redundant lemmas expi_add and expi_zero
2011-09-04 ago remove redundant lemmas about LIMSEQ
2011-09-03 ago remove duplicate lemma finite_choice in favor of finite_set_choice
2011-09-02 ago remove redundant lemma reals_complete2 in favor of complete_real
2011-09-02 ago remove more duplicate lemmas
2011-09-01 ago simplify some proofs about uniform continuity, and add some new ones;
2011-09-01 ago modernize lemmas about 'continuous' and 'continuous_on';
2011-08-28 ago discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-26 ago NEWS entry for setsum_norm ~> norm_setsum
2011-08-25 ago replace some continuous_on lemmas with more general versions
2011-08-25 ago remove legacy theorem Lim_inner
2011-08-25 ago remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
2011-08-25 ago rename subset_{interior,closure} to {interior,closure}_mono;
2011-08-19 ago more concise definition for Inf, Sup on bool
2011-08-18 ago remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-18 ago case_names NEWS
2011-08-10 ago more uniform naming scheme for finite cartesian product type and related theorems
2011-08-09 ago more uniform naming scheme for Inf/INF and Sup/SUP lemmas
2011-08-09 ago merged
2011-08-08 ago dropped lemmas (Inf|Sup)_(singleton|binary)