NEWS
2006-09-19 wenzelm 2006-09-19 * Pure: 'print_theory' now suppresses entities with internal name;
2006-09-19 haftmann 2006-09-19 Operational Equality
2006-09-18 wenzelm 2006-09-18 * Pure: 'class_deps' command visualizes the subclass relation;
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-09-11 haftmann 2006-09-11 hid succ, pred in Numeral.thy
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords
2006-08-14 chaieb 2006-08-14 *** empty log message ***
2006-08-09 wenzelm 2006-08-09 * ProofContext.prems_limit is now -1 by default;
2006-08-08 haftmann 2006-08-08 abandoned equal_list in favor for eq_list
2006-08-03 chaieb 2006-08-03 *** empty log message ***
2006-08-03 ballarin 2006-08-03 Restructured algebra library, added ideals and quotient rings.
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-25 haftmann 2006-07-25 added notes on class_package.ML and codegen_package.ML
2006-07-19 ballarin 2006-07-19 Change to algebra method.
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;