changeset 41526 | 54b4686704af |
parent 39128 | 93a7365fb4ee |
child 42156 | df219e736a5d |
--- a/src/CCL/Set.thy Wed Jan 12 15:53:37 2011 +0100 +++ b/src/CCL/Set.thy Wed Jan 12 16:33:04 2011 +0100 @@ -222,7 +222,7 @@ proof - have "\<not> (EX x. x:A) \<Longrightarrow> A = {}" by (rule equalityI) (blast intro!: subsetI elim!: emptyD)+ - with prems show ?thesis by blast + with assms show ?thesis by blast qed