NEWS
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-02 wenzelm 2014-11-02 added update_header tool;
2014-11-02 wenzelm 2014-11-02 uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;
2014-11-01 wenzelm 2014-11-01 command-line terminator ";" is no longer accepted;
2014-10-31 wenzelm 2014-10-31 discontinued Isar TTY loop;
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-10-28 wenzelm 2014-10-28 'notepad' requires proper nesting of begin/end;
2014-10-26 wenzelm 2014-10-26 clarified default;
2014-10-24 hoelzl 2014-10-24 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
2014-10-24 hoelzl 2014-10-24 move NO_MATCH simproc from the AFP entry Graph_Theory to HOL
2014-10-23 haftmann 2014-10-23 downshift of theory Parity in the hierarchy
2014-10-21 wenzelm 2014-10-21 merged
2014-10-21 wenzelm 2014-10-21 NEWS;
2014-10-21 haftmann 2014-10-21 turn even into an abbreviation
2014-10-20 wenzelm 2014-10-20 official support for "tt" style variants, avoid fragile \verb in LaTeX; official document antiquotation @{verbatim};
2014-10-19 wenzelm 2014-10-19 NEWS;
2014-10-18 wenzelm 2014-10-18 NEWS;
2014-10-14 haftmann 2014-10-14 purely algebraic characterization of even and odd
2014-10-12 haftmann 2014-10-12 generalized and consolidated some theorems concerning divisibility
2014-10-09 haftmann 2014-10-09 more foundational definition for predicate even
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-10-08 wenzelm 2014-10-08 simplified "sos" method;
2014-10-08 Andreas Lochbihler 2014-10-08 move Code_Test to HOL/Library; add corresponding entries in NEWS and CONTRIBUTORS
2014-10-07 wenzelm 2014-10-07 added update_cartouches tool;
2014-10-06 wenzelm 2014-10-06 improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;
2014-10-06 wenzelm 2014-10-06 completion for bibtex entries;
2014-10-05 wenzelm 2014-10-05 NEWS;
2014-10-04 wenzelm 2014-10-04 merged;
2014-10-04 wenzelm 2014-10-04 NEWS;
2014-10-03 wenzelm 2014-10-03 SideKick parser for bibtex entries; tuned signature;
2014-10-03 wenzelm 2014-10-03 context menu for bibtex entries;
2014-10-02 haftmann 2014-10-02 moved lemmas out of Int.thy which have nothing to do with int
2014-09-22 wenzelm 2014-09-22 discontinued old "xnum" token category; simplified Lexicon.read_num, Lexicon.read_float: no sign here; express ZF numerals via "num" with mixfix grammar; recovered printing of ZF numerals: "one" is abbreviation;
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-09-18 blanchet 2014-09-18 updated NEWS
2014-09-18 haftmann 2014-09-18 product over monoids for lists
2014-09-12 haftmann 2014-09-12 NEWS
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 nipkow 2014-09-09 enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-09-07 haftmann 2014-09-07 restrictive options for class dependencies
2014-09-05 blanchet 2014-09-05 updated docs
2014-08-31 haftmann 2014-08-31 restored generic value slot, retaining default behaviour and separate approximate command
2014-08-28 blanchet 2014-08-28 tuned terminology
2014-08-28 blanchet 2014-08-28 moved new para to right section of NEWS
2014-08-28 blanchet 2014-08-28 minor NEWS fix
2014-08-28 blanchet 2014-08-28 updated NEWS
2014-08-28 blanchet 2014-08-28 updated NEWS
2014-08-27 blanchet 2014-08-27 removed not so interesting 'set_empty'
2014-08-19 wenzelm 2014-08-19 merged
2014-08-19 wenzelm 2014-08-19 added PARALLEL_ALLGOALS convenience;
2014-08-19 blanchet 2014-08-19 documented slight incompatibility in NEWS
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-08-16 wenzelm 2014-08-16 updated documentation concerning 'named_theorems';
2014-08-14 wenzelm 2014-08-14 localized command 'method_setup' and 'attribute_setup'; clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed;
2014-08-10 wenzelm 2014-08-10 merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
2014-08-08 wenzelm 2014-08-08 improved monitor panel;
2014-08-04 wenzelm 2014-08-04 tuned;
2014-07-31 wenzelm 2014-07-31 completion popup supports both ENTER and TAB (default);