NEWS
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-03-02 haftmann 2007-03-02 prefix of class interpretation not mandatory any longer
2007-02-28 wenzelm 2007-02-28 added @{const_name}, @{const_syntax};
2007-02-14 haftmann 2007-02-14 added class "preorder"
2007-01-31 haftmann 2007-01-31 dropped lemma duplicates in HOL.thy
2007-01-21 wenzelm 2007-01-21 * ML in Isar: improved error reporting;
2007-01-21 wenzelm 2007-01-21 tuned;
2007-01-20 wenzelm 2007-01-20 * ML within Isar: antiquotations;
2007-01-19 wenzelm 2007-01-19 tuned;
2007-01-19 wenzelm 2007-01-19 tuned;
2006-12-30 wenzelm 2006-12-30 * Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
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