NEWS
2006-05-05 wenzelm 2006-05-05 * Library: theory Accessible_Part has been move to main HOL.
2006-04-30 wenzelm 2006-04-30 * Pure: axclasses now purely definitional; * Pure/kernel: consts certification ignores sort constraints;
2006-04-09 nipkow 2006-04-09 *** empty log message ***
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-03-17 ballarin 2006-03-17 Renamed setsum_mult to setsum_right_distrib.
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-14 wenzelm 2006-03-14 print_statement;
2006-03-14 wenzelm 2006-03-14 Pure: no_translations;
2006-03-13 schirmer 2006-03-13 entry for Library/AssocList
2006-03-10 wenzelm 2006-03-10 tuned;
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-03-08 wenzelm 2006-03-08 tuned;
2006-03-08 wenzelm 2006-03-08 Isar/method: goal restriction;
2006-03-08 nipkow 2006-03-08 *** empty log message ***
2006-02-16 wenzelm 2006-02-16 tuned;
2006-02-16 wenzelm 2006-02-16 tuned;
2006-02-16 wenzelm 2006-02-16 tuned;
2006-02-16 wenzelm 2006-02-16 * Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
2006-02-12 wenzelm 2006-02-12 * ML/Pure/General: improved join interface for tables;
2006-02-12 wenzelm 2006-02-12 tuned;
2006-02-10 wenzelm 2006-02-10 * ML/Pure: generic Args/Attrib syntax everywhere;
2006-02-08 nipkow 2006-02-08 *** empty log message ***
2006-02-02 wenzelm 2006-02-02 tuned;
2006-02-02 wenzelm 2006-02-02 * Isar: 'obtains' element;
2006-01-31 wenzelm 2006-01-31 * Pure: 'advanced' translation functions use Context.generic instead of just theory;
2006-01-28 wenzelm 2006-01-28 Pure/Isar: (un)folded, (un)fold, unfolding support object-level rewrite rules; ML/Isar: installed ML toplevel pretty printer for type Proof.context;
2006-01-21 wenzelm 2006-01-21 tuned;
2006-01-21 wenzelm 2006-01-21 * ML: simplified type attribute;
2006-01-19 wenzelm 2006-01-19 * ML/Isar: theory setup has type (theory -> theory);
2006-01-15 wenzelm 2006-01-15 tuned;
2006-01-15 wenzelm 2006-01-15 tuned;
2006-01-15 wenzelm 2006-01-15 * Classical: optional weight for attributes; * HOL: prefer ex1I over ex_ex1I in single-step reasoning;
2006-01-14 wenzelm 2006-01-14 tuned;
2006-01-14 wenzelm 2006-01-14 * ML/Isar: simplified treatment of user-level errors;
2006-01-13 nipkow 2006-01-13 *** empty log message ***
2006-01-10 wenzelm 2006-01-10 tuned;
2006-01-10 wenzelm 2006-01-10 * ML: generic context, data, attributes;
2006-01-07 wenzelm 2006-01-07 * Provers/induct: improved simultaneous goals -- nested cases;
2006-01-06 wenzelm 2006-01-06 Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
2006-01-04 wenzelm 2006-01-04 tuned;
2006-01-04 wenzelm 2006-01-04 * Pure/Isar: Toplevel.theory_theory_to_proof;
2006-01-03 paulson 2006-01-03 Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed
2006-01-03 haftmann 2006-01-03 rearranged burrow_split to fold_burrow to allow composition with fold_map
2006-01-03 wenzelm 2006-01-03 * Pure/Isar: new command 'unfolding'; * ML/Provers: more generic wrt. syntax of object-logics; tuned;
2005-12-31 wenzelm 2005-12-31 * Provers/classical: removed obsolete classical version of elim_format;
2005-12-23 wenzelm 2005-12-23 tuned;
2005-12-23 wenzelm 2005-12-23 * Provers/induct: support simultaneous goals with mutual rules;
2005-12-23 haftmann 2005-12-23 is_prefix
2005-12-22 wenzelm 2005-12-22 tuned;
2005-12-22 wenzelm 2005-12-22 * induct: improved treatment of mutual goals and mutual rules;
2005-12-21 haftmann 2005-12-21 discontinued unflat in favour of burrow and burrow_split
2005-12-20 wenzelm 2005-12-20 tuned;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-13 wenzelm 2005-12-13 Provers/induct: coinduct; HOL/Library: theory Coinductive_List;
2005-12-08 wenzelm 2005-12-08 removed hint for Classical.swap, which is not really user-level anyway;
2005-12-08 wenzelm 2005-12-08 * HOL: Theorem 'swap' is no longer bound at the ML top-level.
2005-11-30 wenzelm 2005-11-30 simulaneous 'def';
2005-11-27 wenzelm 2005-11-27 * Provers/induct: obtain pattern;
2005-11-25 wenzelm 2005-11-25 tuned;
2005-11-23 wenzelm 2005-11-23 tuned;