NEWS
2006-12-22 ballarin 2006-12-22 Experimenting with interpretations of "definition".
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-12 huffman 2006-12-12 additions to HOL-Complex
2006-12-10 wenzelm 2006-12-10 added print_abbrevs; tuned;
2006-12-09 wenzelm 2006-12-09 added antiquotation abbrev;
2006-12-05 wenzelm 2006-12-05 * Pure: official theorem names and additional comments are now strictly separate.
2006-11-29 wenzelm 2006-11-29 tuned;
2006-11-27 haftmann 2006-11-27 adjusted syntax for internal code generation
2006-11-26 wenzelm 2006-11-26 * Pure: syntax constant for foo (binder) is called foo_binder;
2006-11-22 wenzelm 2006-11-22 * settings: ML_IDENTIFIER includes the Isabelle version identifier;
2006-11-22 haftmann 2006-11-22 added Isar syntax for adding parameters to axclasses
2006-11-21 wenzelm 2006-11-21 * Isar: the assumptions of a long theorem statement are available as assms;
2006-11-18 haftmann 2006-11-18 adjustments for class package
2006-11-14 wenzelm 2006-11-14 tuned antiquotation theory;
2006-11-13 wenzelm 2006-11-13 tuned;
2006-11-13 haftmann 2006-11-13 added antiquotation theory
2006-11-13 krauss 2006-11-13 updated
2006-11-11 wenzelm 2006-11-11 * Local theory targets ``context/locale/class ... begin'' followed by ``end''.
2006-11-09 wenzelm 2006-11-09 HOL: less/less_eq on bool, modified syntax;
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-11-08 wenzelm 2006-11-08 moved contribution note to CONTRIBUTORS;
2006-11-08 krauss 2006-11-08 Made "termination by lexicographic_order" the default for "fun" definitions.
2006-11-07 schirmer 2006-11-07 field-update in records is generalised to take a function on the field rather than the new value.
2006-11-07 haftmann 2006-11-07 made locale partial_order compatible with axclass order
2006-11-07 wenzelm 2006-11-07 'const_syntax' command: allow fixed variables, renamed to 'notation';
2006-11-07 krauss 2006-11-07 updated NEWS
2006-11-04 wenzelm 2006-11-04 tuned;
2006-10-31 haftmann 2006-10-31 adapted to new serializer syntax
2006-10-31 haftmann 2006-10-31 dropped nth_update
2006-10-23 haftmann 2006-10-23 (added entry)
2006-10-20 haftmann 2006-10-20 Symtab.foldl replaced by Symtab.fold
2006-10-16 ballarin 2006-10-16 Order and lattice structures no longer based on records.
2006-10-11 wenzelm 2006-10-11 * isabelle-process: option -S (secure mode) disables some critical operations;
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-09 wenzelm 2006-10-09 attribute "symmetric": standardized schematic variables;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-10-01 wenzelm 2006-10-01 tuned;
2006-09-26 krauss 2006-09-26 Changed precedence of "op O" (relation composition) from 60 to 75.
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly
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;