NEWS
2005-09-28 wenzelm revert 'defs' advertisement;
2005-09-27 wenzelm more details about incomplete 'defs';
2005-09-27 wenzelm tuned;
2005-09-27 berghofe Added entries for code_module, code_library, and value.
2005-09-25 wenzelm * Hyperreal: A theory of Taylor series.
2005-09-23 webertj new sat tactic
2005-09-23 wenzelm tuned;
2005-09-23 paulson ATP linkup
2005-09-22 nipkow *** empty log message ***
2005-09-22 huffman HOLCF theorem naming conventions
2005-09-21 haftmann added AList.make, eq_fst, apr ...
2005-09-21 wenzelm tunes;
2005-09-20 wenzelm tuned;
2005-09-20 wenzelm tuned;
2005-09-20 wenzelm tuned;
2005-09-20 wenzelm HOL/ex/Chinese.thy;
2005-09-20 haftmann infix operator precedence
2005-09-17 wenzelm HTML.with_charset;
2005-09-17 wenzelm Cube: converted to Isar, use locales;
2005-09-16 huffman add HOLCF entries for pcpodef, cont_proc, fixrec;
2005-09-16 ballarin tuned
2005-09-15 wenzelm * Improved efficiency of the Simplifier etc.;
2005-09-15 wenzelm incorporated HOL/Hyperreal/CHANGES;
2005-09-15 wenzelm command 'thms_containing' has been discontinued in favour of 'find_theorems';
2005-09-15 haftmann AList, the_*
2005-09-14 wenzelm tuned;
2005-09-14 wenzelm hide: added option '(open)';
2005-09-14 schirmer ... prem19
2005-09-14 wenzelm Method comm_ring for proving equalities in commutative rings.
2005-09-14 wenzelm HOL: method comm_ring;
2005-09-13 wenzelm tuned;
2005-09-06 wenzelm axclass: name space prefix is now "c_class" instead of just "c";
2005-09-05 wenzelm tuned;
2005-09-05 wenzelm Markup commands 'chapter' .. 'text' support optional locale specification;
2005-09-02 ballarin print_locale omits facts by default
2005-08-31 wenzelm * Delimiters of outer tokens now produce separate LaTeX macros;
2005-08-30 paulson patterns in setsum and setprod
2005-08-28 wenzelm * ML functions legacy_bindings and use_legacy_bindings;
2005-08-28 wenzelm tuned;
2005-08-24 ballarin Printing of interpretations: option to show witness theorems;
2005-08-18 wenzelm * The ML antiquotation prints type-checked ML expressions verbatim.
2005-08-18 wenzelm * Proper output of proof terms within a proof context;
2005-08-17 ballarin Interpretation in locales.
2005-08-17 nipkow *** empty log message ***
2005-08-16 wenzelm * Command tags control specific markup of certain regions of text (replaces usedir -H);
2005-08-03 avigad mentioned change to exp_ge_add_one_self, new transitivity rules
2005-08-01 wenzelm * Pure/Simplifier: improved handling of bound variables;
2005-07-29 avigad mentioned Ln in NEWS
2005-07-28 wenzelm tuned;
2005-07-25 avigad Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
2005-07-19 wenzelm tuned;
2005-07-19 avigad added list of theorem changes to NEWS
2005-07-18 haftmann reverted from fold_yield to fold_map
2005-07-15 wenzelm *** empty log message ***
2005-07-15 wenzelm * Pure/library.ML: several combinators for linear functional transformations;
2005-07-14 wenzelm * Improved 'oracle' command -- type-safe;
2005-07-13 wenzelm * Isar session: The initial use of ROOT.ML is now always timed;
2005-07-06 wenzelm * Pure: Output.time_accumulator;
2005-07-06 wenzelm isatool fixheaders;
2005-07-05 wenzelm tuned;
less more (0) -300 -100 -60 tip