src/HOL/Set.thy
changeset 30814 10dc9bc264b7
parent 30596 140b22f22071
child 31166 a90fe83f58ea
--- 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