--- a/src/HOL/Set.thy Tue Mar 31 12:07:17 2009 +0200 +++ b/src/HOL/Set.thy Tue Mar 31 13:23:39 2009 +0200 @@ -2384,7 +2384,7 @@ unfolding Inf_bool_def by auto lemma not_Sup_empty_bool [simp]: - "\<not> Sup {}" + "\<not> \<Squnion>{}" unfolding Sup_bool_def by auto