--- a/src/ZF/ZF_Base.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/ZF/ZF_Base.thy Tue Jan 16 09:30:00 2018 +0100
@@ -635,8 +635,8 @@
declare Pow_iff [iff]
-lemmas Pow_bottom = empty_subsetI [THEN PowI] \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close>
-lemmas Pow_top = subset_refl [THEN PowI] \<comment>\<open>@{term"A \<in> Pow(A)"}\<close>
+lemmas Pow_bottom = empty_subsetI [THEN PowI] \<comment> \<open>@{term"0 \<in> Pow(B)"}\<close>
+lemmas Pow_top = subset_refl [THEN PowI] \<comment> \<open>@{term"A \<in> Pow(A)"}\<close>
subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>