# HG changeset patch
# User haftmann
# Date 1265807550 3600
# Node ID 5acba118b02a37c8286ef72a73492e8de77c6ff1
# Parent cfe605c54e5096952f5f9b1440841c0104a1da4c
NEWS
diff r cfe605c54e50 r 5acba118b02a NEWS
 a/NEWS Wed Feb 10 14:12:04 2010 +0100
+++ b/NEWS Wed Feb 10 14:12:30 2010 +0100
@@ 22,6 +22,8 @@
* Some generic constants have been put to appropriate theories:
+ less_eq, less: Orderings
+ abs, sgn: Groups
inverse, divide: Rings
INCOMPATIBILITY.
@@ 80,13 +82,9 @@
INCOMPATIBILITY.
* Index syntax for structures must be imported explicitly from library
theory Structure_Syntax. INCOMPATIBILITY.

* New theory Algebras contains generic algebraic structures and
generic algebraic operations. INCOMPATIBILTY: constants zero, one,
plus, minus, uminus, times, abs, sgn, less_eq and
less have been moved from HOL.thy to Algebras.thy.
+plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy.
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.