NEWS
changeset 75963 884dbbc8e1b3
parent 75951 97e7bb231981
child 75967 ff164add75cd
child 75975 44e0ba464e08
--- a/NEWS	Wed Aug 24 06:21:06 2022 +0000
+++ b/NEWS	Wed Aug 24 08:22:13 2022 +0000
@@ -44,6 +44,14 @@
 
 *** HOL ***
 
+* HOL-Algebra: Facts renamed to avoid fact name clashes on interpretation:
+
+    is_ring ~> ring_axioms
+    cring ~> cring_axioms
+    R_def ~> R_m_def
+
+INCOMPATIBILITY.
+
 * Moved auxiliary computation constant "divmod_nat" to theory
 "Euclidean_Division".  Minor INCOMPATIBILITY.