NEWS
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2010-03-03 wenzelm 2010-03-03 authentic syntax for *all* logical entities;
2010-03-01 wenzelm 2010-03-01 added type_notation command;
2010-02-27 wenzelm 2010-02-27 clarified @{const_name} (only logical consts) vs. @{const_abbrev}; tuned;
2010-02-27 wenzelm 2010-02-27 ML antiquotations for type classes;
2010-02-26 haftmann 2010-02-26 merged
2010-02-24 haftmann 2010-02-24 renamed theory Rational to Rat
2010-02-25 wenzelm 2010-02-25 more orthogonal antiquotations for type constructors;
2010-02-24 wenzelm 2010-02-24 allow general mixfix syntax for type constructors;
2010-02-22 haftmann 2010-02-22 NEWS
2010-02-22 haftmann 2010-02-22 NEWS
2010-02-22 haftmann 2010-02-22 merged
2010-02-22 haftmann 2010-02-22 NEWS
2010-02-19 haftmann 2010-02-19 NEWS
2010-02-19 haftmann 2010-02-19 NEWS
2010-02-21 wenzelm 2010-02-21 tuned;
2010-02-21 wenzelm 2010-02-21 NEWS: authentic syntax for *all* term constants;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2010-02-11 wenzelm 2010-02-11 added ML antiquotation @{syntax_const};
2010-02-10 wenzelm 2010-02-10 renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
2010-02-10 haftmann 2010-02-10 NEWS
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 NEWS: ax_simps
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate theory for index structures
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-02-06 wenzelm 2010-02-06 misc tuning;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2010-01-22 haftmann 2010-01-22 HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2010-01-22 haftmann 2010-01-22 NEWS
2010-01-19 hoelzl 2010-01-19 Add transpose to the List-theory.
2010-01-04 wenzelm 2010-01-04 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 wenzelm 2010-01-04 discontinued old ISABELLE and ISATOOL environment settings;
2010-01-04 wenzelm 2010-01-04 discontinued special HOL_USEDIR_OPTIONS;
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum; corrected spelling
2009-12-11 wenzelm 2009-12-11 Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution; tuned;
2009-12-11 haftmann 2009-12-11 NEWS
2009-12-05 haftmann 2009-12-05 tuned lattices theory fragements; generlized some lemmas from sets to lattices
2009-12-04 haftmann 2009-12-04 merged, resolving minor conflicts
2009-12-04 haftmann 2009-12-04 NEWS
2009-12-04 wenzelm 2009-12-04 back to after-release mode;
2009-11-23 wenzelm 2009-11-23 more tuning for release;
2009-11-23 haftmann 2009-11-23 tuned NEWS
2009-11-22 haftmann 2009-11-22 more uniform view on various number theory refinement steps
2009-11-22 wenzelm 2009-11-22 more NEWS, more tuning for release;
2009-11-22 wenzelm 2009-11-22 misc tuning and updates for official release;
2009-11-21 kleing 2009-11-21 wwwfind support currently for Linux only
2009-11-20 huffman 2009-11-20 NEWS: HOLCF changes since the last release
2009-11-20 kleing 2009-11-20 added NEWS item for wwwfind
2009-11-19 hoelzl 2009-11-19 Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
2009-11-13 nipkow 2009-11-13 -
2009-11-12 bulwahn 2009-11-12 added a tabled implementation of the reflexive transitive closure
2009-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-11-12 bulwahn 2009-11-12 announcing the predicate compiler in NEWS and CONTRIBUTORS
2009-11-08 wenzelm 2009-11-08 updated functor Theory_Data, Proof_Data, Generic_Data;