Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added "no_atp" to Cantor's paradox
authorblanchet
Tue, 05 Apr 2011 11:44:34 +0200
changeset 42238 d53dccb38dd1
parent 42237 e645d7255bd4
child 42239 e48baf91aeab
added "no_atp" to Cantor's paradox
src/HOL/Fun.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle