updated NEWS w.r.t. e0237f2eb49d
--- a/NEWS Sun Mar 08 17:07:49 2020 +0000
+++ b/NEWS Tue Mar 10 14:16:19 2020 +0100
@@ -89,6 +89,12 @@
*** HOL ***
+* Removed multiplicativity assumption from normalization_semidom typeclass.
+ Introduced various new intermediate typeclasses with the multiplicativity
+ assumption; many theorem statements (especially involving GCD/LCM) had
+ to be adapted. This allows for a more natural instantiation of the
+ algebraic typeclasses for e.g. Gaussian integers. INCOMPATIBILITY.
+
* Improvements of the 'lift_bnf' command:
- Add support for quotient types.
- Generate transfer rules for the lifted map/set/rel/pred constants