src/HOL/Library/Saturated.thy

--- a/src/HOL/Library/Saturated.thy	Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Saturated.thy	Thu Jul 25 08:57:16 2013 +0200
@@ -263,6 +263,12 @@
   note finite
   moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   ultimately show "Sup A \<le> z" by (induct A) auto
+next
+  show "Inf {} = (top::'a sat)"
+    by (auto simp: top_sat_def)
+next
+  show "Sup {} = (bot::'a sat)"
+    by (auto simp: bot_sat_def)
 qed
 
 hide_const (open) sat_of_nat