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)
2011-08-08 ago rename type 'a net to 'a filter, following standard mathematical terminology
2011-08-04 ago NEWS
2011-08-03 ago NEWS
2011-08-02 ago Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
2011-08-02 ago NEWS: fix typo
2011-08-02 ago NEWS
2011-07-25 ago merged
2011-07-24 ago more coherent structure in and across theories
2011-07-25 ago NEWS
2011-07-20 ago class complete_linorder
2011-07-18 ago avoid misunderstandable names
2011-07-17 ago more on complement
2011-07-17 ago more consistent theorem names
2011-07-17 ago further generalization from sets to complete lattices
2011-07-13 ago uniqueness lemmas for bot and top
2011-07-13 ago adjusted to tightened specification of classes bot and top
2011-07-11 ago NEWS;
2011-07-10 ago merged;
2011-07-10 ago improved NEWS
2011-07-09 ago NEWS
2011-07-10 ago inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
2011-07-08 ago discontinued special treatment of hard tabulators;
2011-07-01 ago update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
2011-07-01 ago adding a minimalistic documentation of the value antiquotation in the Isar reference manual
2011-06-27 ago merged
2011-06-27 ago minor Sledgehammer news
2011-06-27 ago document changes to Sledgehammer and "try"
2011-06-27 ago NEWS;
2011-06-23 ago Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
2011-06-09 ago NEWS
2011-06-07 ago obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-06 ago marked "metisF" as legacy -- nobody uses it or needs it
2011-05-20 ago added Isabelle_Process.is_active;
2011-05-20 ago NEWS
2011-05-18 ago NEWS
2011-05-15 ago NEWS (cf. 4e8483cc2cc5);
2011-05-14 ago use pointfree characterisation for fold_set locale
2011-05-13 ago proper Proof.context for classical tactics;
2011-05-12 ago renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
2011-05-12 ago added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-05 ago tuned;
2011-05-03 ago more conventional naming scheme: names_long, names_short, names_unique;
2011-05-03 ago some documentation of @{rail} antiquotation;
2011-05-02 ago NEWS;
2011-05-01 ago document new type system syntax