added "no_atp" to Cantor's paradox
authorblanchet
Tue Apr 05 11:44:34 2011 +0200 (2011-04-05)
changeset 42238d53dccb38dd1
parent 42237 e645d7255bd4
child 42239 e48baf91aeab
added "no_atp" to Cantor's paradox
src/HOL/Fun.thy
     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