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.