NEWS
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-19 haftmann 2009-06-19 merged
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-19 nipkow 2009-06-19 NewNumberTheory
2009-06-15 haftmann 2009-06-15 authentic syntax for Pow and image
2009-06-13 haftmann 2009-06-13 merged
2009-06-13 haftmann 2009-06-13 quickcheck using generic code generator
2009-06-10 wenzelm 2009-06-10 discontinued escaped symbols; tuned;
2009-06-08 haftmann 2009-06-08 method linarith
2009-05-31 wenzelm 2009-05-31 removed "compress" option from isabelle-process and isabelle usedir -- this is always enabled;
2009-05-31 wenzelm 2009-05-31 discontinued support for Poly/ML 4.x versions;
2009-05-30 wenzelm 2009-05-30 eliminated old Attrib.add_attributes (and Attrib.syntax);
2009-05-30 wenzelm 2009-05-30 eliminated old Method.add_method(s);
2009-04-27 haftmann 2009-04-27 cleaned up theory power further
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-22 haftmann 2009-04-22 dropped duplication
2009-04-22 haftmann 2009-04-22 code_datatype and power
2009-04-20 haftmann 2009-04-20 merged
2009-04-20 haftmann 2009-04-20 changes in power operations
2009-04-17 haftmann 2009-04-17 formal declaration of undefined parameters after class instantiation
2009-04-17 haftmann 2009-04-17 separated funpow, relpow from power on monoids
2009-04-16 haftmann 2009-04-16 tightended specification of class semiring_div
2009-04-20 wenzelm 2009-04-20 back to non-release mode;
2009-04-02 wenzelm 2009-04-02 some more HOL-Nominal news;
2009-04-02 wenzelm 2009-04-02 some HOL-Nominal news;
2009-04-02 wenzelm 2009-04-02 tuned;
2009-04-02 wenzelm 2009-04-02 misc cleanup and rearrangements for Isabelle2009 release;
2009-03-27 haftmann 2009-03-27 merged
2009-03-27 haftmann 2009-03-27 dropped toy example Code_Antiq
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default; misc tuning and updates;
2009-03-24 nipkow 2009-03-24 NEWS: [arith]
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-19 wenzelm 2009-03-19 tuned;
2009-03-16 huffman 2009-03-16 document new additions to HOL/Library
2009-03-16 wenzelm 2009-03-16 simplifief 'method_setup' command;
2009-03-15 wenzelm 2009-03-15 merged
2009-03-14 immler 2009-03-14 updated NEWS
2009-03-15 wenzelm 2009-03-15 simplified attribute and method setup;
2009-03-11 wenzelm 2009-03-11 added 'local_setup' command; tuned;
2009-03-11 hoelzl 2009-03-11 Updated paths in Decision_Procs comments and NEWS
2009-03-10 webertj 2009-03-10 Instead of giving up entirely, arith now ignores all inequalities when there are too many.
2009-03-09 wenzelm 2009-03-09 tuned;
2009-03-09 wenzelm 2009-03-09 * More systematic treatment of long names, abstract name bindings, and name space operations. * Simplified interface for defining document antiquotations via ThyOutput.antiquotation.
2009-03-06 haftmann 2009-03-06 constructive version of Cantor's first diagonalization argument
2009-03-06 haftmann 2009-03-06 merged
2009-03-05 haftmann 2009-03-05 merged
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-03-06 haftmann 2009-03-06 corrected slip in NEWS
2009-03-06 haftmann 2009-03-06 added strict_mono predicate
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04 wenzelm 2009-03-04 NEWS: renamed o2s to Option.set;
2009-03-04 nipkow 2009-03-04 Made Option a separate theory and renamed option_map to Option.map
2009-03-03 nipkow 2009-03-03 removed and renamed redundant lemmas
2009-03-02 nipkow 2009-03-02 name fix
2009-03-02 nipkow 2009-03-02 name changes
2009-03-01 nipkow 2009-03-01 removed redundant lemmas
2009-02-28 huffman 2009-02-28 add news for HOLCF; fixed some typos and inaccuracies
2009-02-28 wenzelm 2009-02-28 * New prover for coherent logic (see src/Tools/coherent.ML).
2009-02-26 wenzelm 2009-02-26 tuned NEWS;