# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1746357507 -3600
# Node ID 328de89f20f9e54a17dc3f2f6c958ad91d76bb62
# Parent  267db8c321c4d5515f8c7bf4ede510bc2c6edd2a
More type class things

diff -r 267db8c321c4 -r 328de89f20f9 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Fri May 02 17:24:43 2025 +0200
+++ b/src/HOL/Groups_List.thy	Sun May 04 12:18:27 2025 +0100
@@ -665,4 +665,7 @@
   "prod_list xs = 0 \<longleftrightarrow> (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) \<in> set xs"
   by (induction xs) simp_all
 
+lemma prod_list_nonneg: "(\<And> x. (x :: 'a :: ordered_semiring_1) \<in> set xs \<Longrightarrow> x \<ge> 0) \<Longrightarrow> prod_list xs \<ge> 0"
+  by (induct xs) auto
+
 end
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