src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/HOL/Orderings.thy	Sun Apr 27 11:20:39 2025 +0100
@@ -1307,6 +1307,9 @@
 
 class unbounded_dense_linorder = dense_linorder + no_top + no_bot
 
+class unbounded_dense_order = dense_order + no_top + no_bot
+
+instance unbounded_dense_linorder \<subseteq> unbounded_dense_order ..
 
 subsection \<open>Wellorders\<close>