NEWS
2007-06-10 nipkow 2007-06-10 *** empty log message ***
2007-06-08 chaieb 2007-06-08 Method "algebra" solves polynomial equations over (semi)rings
2007-06-05 haftmann 2007-06-05 moved generic algebra modules
2007-06-03 nipkow 2007-06-03 *** empty log message ***
2007-06-01 haftmann 2007-06-01 fixed typo
2007-05-30 haftmann 2007-05-30 tuned
2007-05-28 huffman 2007-05-28 Complex: generalized type of exp
2007-05-25 nipkow 2007-05-25 *** empty log message ***
2007-05-25 nipkow 2007-05-25 *** empty log message ***
2007-05-25 nipkow 2007-05-25 *** empty log message ***
2007-05-19 haftmann 2007-05-19 constant op @ now named append
2007-05-19 nipkow 2007-05-19 *** empty log message ***
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-05-14 huffman 2007-05-14 generalized sgn function to work on any real normed vector space
2007-05-14 huffman 2007-05-14 root and sqrt on negative inputs
2007-05-14 webertj 2007-05-14 ProofGeneral: Find Theorems search form
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-08 wenzelm 2007-05-08 tuned;
2007-05-08 wenzelm 2007-05-08 tuned context data;
2007-05-07 wenzelm 2007-05-07 * Context data interfaces;
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-30 wenzelm 2007-04-30 explicit treatment of legacy_features;
2007-04-26 haftmann 2007-04-26 moved code generation pretty integers and characters to separate theories
2007-04-20 haftmann 2007-04-20 clarifed
2007-04-20 haftmann 2007-04-20 code generator changes
2007-03-16 haftmann 2007-03-16 lattice cleanup
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.