changeset 42238 | d53dccb38dd1 |
parent 41657 | 89451110ba8e |
child 42903 | ec9eb1fbfcb8 |
--- a/src/HOL/Fun.thy Tue Apr 05 11:39:48 2011 +0200 +++ b/src/HOL/Fun.thy Tue Apr 05 11:44:34 2011 +0200 @@ -770,7 +770,7 @@ subsection {* Cantor's Paradox *} -lemma Cantors_paradox: +lemma Cantors_paradox [no_atp]: "\<not>(\<exists>f. f ` A = Pow A)" proof clarify fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast