src/HOL/Conditionally_Complete_Lattices.thy

--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 12 15:11:20 2020 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue May 12 16:53:02 2020 +0100
@@ -563,6 +563,10 @@
   shows "Inf K \<in> K"
 by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)
 
+lemma Sup_nat_empty [simp]: "Sup {} = (0::nat)"
+  by (auto simp add: Sup_nat_def) 
+
+
 
 instantiation int :: conditionally_complete_linorder
 begin