--- a/NEWS Fri Feb 05 14:33:50 2010 +0100
+++ b/NEWS Mon Feb 08 14:06:41 2010 +0100
@@ -12,7 +12,7 @@
*** HOL ***
-* more consistent naming of type classes involving orderings (and lattices):
+* More consistent naming of type classes involving orderings (and lattices):
lower_semilattice ~> semilattice_inf
upper_semilattice ~> semilattice_sup
@@ -33,12 +33,6 @@
pordered_ring_abs ~> ordered_ring_abs
pordered_semiring ~> ordered_semiring
- lordered_ab_group_add ~> lattice_ab_group_add
- lordered_ab_group_add_abs ~> lattice_ab_group_add_abs
- lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add
- lordered_ab_group_add_join ~> semilattice_sup_ab_group_add
- lordered_ring ~> lattice_ring
-
ordered_ab_group_add ~> linordered_ab_group_add
ordered_ab_semigroup_add ~> linordered_ab_semigroup_add
ordered_cancel_ab_semigroup_add ~> linordered_cancel_ab_semigroup_add
@@ -58,6 +52,15 @@
ordered_semiring_1_strict ~> linordered_semiring_1_strict
ordered_semiring_strict ~> linordered_semiring_strict
+ The following slightly odd type classes have been moved to
+ a separate theory Library/Lattice_Algebras.thy:
+
+ lordered_ab_group_add ~> lattice_ab_group_add
+ lordered_ab_group_add_abs ~> lattice_ab_group_add_abs
+ lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add
+ lordered_ab_group_add_join ~> semilattice_sup_ab_group_add
+ lordered_ring ~> lattice_ring
+
INCOMPATIBILITY.
* new theory Algebras.thy contains generic algebraic structures and