diff -r 267db8c321c4 -r 328de89f20f9 src/HOL/Rings.thy --- 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