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