NEWS
2007-07-31 wenzelm 2007-07-31 * Configuration options; * Named collections of theorems;
2007-07-28 wenzelm 2007-07-28 * Isar: command 'declaration'; * Isar: proper interfaces for simplification procedures; * Isar: an extra pair of brackets around attribute declarations abbreviates a theorem reference involving an internal dummy fact;
2007-07-25 ballarin 2007-07-25 tuned
2007-07-24 krauss 2007-07-24 renamed lemma "set_take_whileD" to "set_takeWhileD"
2007-07-23 ballarin 2007-07-23 interpretation: unfolding of equations;
2007-07-20 wenzelm 2007-07-20 tuned;
2007-07-20 wenzelm 2007-07-20 * Theory loader: be more serious about observing the static theory header specifications; * Theory loader: optional support for content-based file identification;
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-07-19 haftmann 2007-07-19 updated
2007-07-11 berghofe 2007-07-11 Added entry for new inductive definition package.
2007-07-04 nipkow 2007-07-04 *** empty log message ***
2007-07-04 nipkow 2007-07-04 *** empty log message ***
2007-07-03 wenzelm 2007-07-03 tuned;
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;