author | wenzelm |
Tue, 31 Mar 2009 13:23:39 +0200 | |
changeset 30816 | 10dc9bc264b7 |
parent 30813 | a0863fcd9bbf |
child 30817 | e96498265a05 |
src/HOL/Set.thy | file | annotate | diff | comparison | revisions |
1.1 --- a/src/HOL/Set.thy Tue Mar 31 12:07:17 2009 +0200 1.2 +++ b/src/HOL/Set.thy Tue Mar 31 13:23:39 2009 +0200 1.3 @@ -2384,7 +2384,7 @@ 1.4 unfolding Inf_bool_def by auto 1.5 1.6 lemma not_Sup_empty_bool [simp]: 1.7 - "\<not> Sup {}" 1.8 + "\<not> \<Squnion>{}" 1.9 unfolding Sup_bool_def by auto 1.10 1.11