NEWS
2006-07-17 webertj 2006-07-17 support for MiniSat proof traces added
2006-07-12 wenzelm 2006-07-12 * Isar: ":" (colon) is no longer a symbolic identifier character;
2006-07-11 wenzelm 2006-07-11 * Pure: structure Name;
2006-07-11 kleing 2006-07-11 hex and binary numerals (contributed by Rafal Kolanski)
2006-07-08 wenzelm 2006-07-08 * Pure: structure Variable provides operations for proper treatment of fixed/schematic variables; * Pure: Goal.prove, Goal.prove_global; tuned;
2006-07-04 wenzelm 2006-07-04 Isar: 'print_facts' prints all local facts;
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2006-06-15 nipkow 2006-06-15 *** empty log message ***
2006-06-12 berghofe 2006-06-12 Added "evaluation" method.
2006-06-07 wenzelm 2006-06-07 * Theory syntax: some popular names (e.g. "class", "if") are now keywords. * Isar: schematic goals are no longer restricted to higher-order patterns. * ML/Pure: Logic.(un)varify only works in a global context, which is now enforced.
2006-06-06 ballarin 2006-06-06 Improved parameter management of locales.
2006-05-24 wenzelm 2006-05-24 tuned;
2006-05-24 wenzelm 2006-05-24 tuned;
2006-05-24 wenzelm 2006-05-24 Pure: update on overloaded defs;
2006-05-17 wenzelm 2006-05-17 * Pure: syntax 'CONST name' produces a fully internalized constant; tuned;
2006-05-16 wenzelm 2006-05-16 * Isar/locale: 'const_syntax';
2006-05-16 wenzelm 2006-05-16 * Pure/library: divide_and_conquer; * Theory Real: new method ferrack;
2006-05-13 wenzelm 2006-05-13 * Pure: overloaded definitions are now actually checked for acyclic dependencies;
2006-05-07 wenzelm 2006-05-07 * Isar: removed obsolete 'concl is' patterns.
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;