--- a/src/HOL/Rings.thy Fri May 02 17:24:43 2025 +0200
+++ b/src/HOL/Rings.thy Sun May 04 12:18:27 2025 +0100
@@ -1987,6 +1987,8 @@
subclass ordered_semiring_0 ..
+subclass ordered_cancel_ab_semigroup_add ..
+
end
class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add