src/HOL/Fun.thy
changeset 54147 97a8ff4e4ac9
parent 53927 abe2b313f0e5
child 54578 9387251b6a46
     1.1 --- a/src/HOL/Fun.thy	Fri Oct 18 10:35:57 2013 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Oct 18 10:43:20 2013 +0200
     1.3 @@ -775,7 +775,7 @@
     1.4  
     1.5  subsection {* Cantor's Paradox *}
     1.6  
     1.7 -lemma Cantors_paradox [no_atp]:
     1.8 +lemma Cantors_paradox:
     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