NEWS
2007-06-27 nipkow 2007-06-27 *** empty log message ***
2007-06-25 obua 2007-06-25 commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-24 nipkow 2007-06-24 *** empty log message ***
2007-06-21 huffman 2007-06-21 changed simp rules for of_nat
2007-06-21 paulson 2007-06-21 integration of Metis prover
2007-06-14 wenzelm 2007-06-14 updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
2007-06-13 huffman 2007-06-13 int abbreviates of_nat
2007-06-13 wenzelm 2007-06-13 * Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account; * Isar: implicit use of prems from the Isar proof context is considered a legacy feature;
2007-06-13 wenzelm 2007-06-13 tuned;
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;