--- a/NEWS Thu Aug 18 09:29:11 2022 +0200
+++ b/NEWS Wed Aug 17 20:37:16 2022 +0000
@@ -39,7 +39,7 @@
* New Theory Code_Abstract_Char implements characters by target language
integers, sacrificing pattern patching in exchange for dramatically
-increased performance for comparisions.
+increased performance for comparisons.
* New theory HOL-Library.NList of fixed length lists
@@ -49,6 +49,9 @@
* Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
longer. INCOMPATIBILITY.
+* Streamlined primitive definitions of division and modulus on integers.
+INCOMPATIBILITY.
+
* Theory "HOL.Fun":
- Added predicate monotone_on and redefined monotone to be an
abbreviation. Lemma monotone_def is explicitly provided for backward