# HG changeset patch
# User blanchet
# Date 1301996674 -7200
# Node ID d53dccb38dd1cb93e511e8567a81d8fabd5aaefe
# Parent  e645d7255bd455174d96591936d18c5d693b40b5
added "no_atp" to Cantor's paradox

diff -r e645d7255bd4 -r d53dccb38dd1 src/HOL/Fun.thy
--- 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