diff -r 458b4e3720ab -r 27f3c10b0b50 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/ZF.thy	Mon Dec 07 10:23:50 2015 +0100
@@ -15,9 +15,9 @@
 instance i :: "term" ..
 
 axiomatization
-  zero :: "i"  ("0")   --\<open>the empty set\<close>  and
-  Pow :: "i => i"  --\<open>power sets\<close>  and
-  Inf :: "i"  --\<open>infinite set\<close>
+  zero :: "i"  ("0")   \<comment>\<open>the empty set\<close>  and
+  Pow :: "i => i"  \<comment>\<open>power sets\<close>  and
+  Inf :: "i"  \<comment>\<open>infinite set\<close>
 
 text \<open>Bounded Quantifiers\<close>
 consts
@@ -56,7 +56,7 @@
   Pair  :: "[i, i] => i"
   fst   :: "i => i"
   snd   :: "i => i"
-  split :: "[[i, i] => 'a, i] => 'a::{}"  --\<open>for pattern-matching\<close>
+  split :: "[[i, i] => 'a, i] => 'a::{}"  \<comment>\<open>for pattern-matching\<close>
 
 text \<open>Sigma and Pi Operators\<close>
 consts
@@ -69,35 +69,35 @@
   range       :: "i => i"
   field       :: "i => i"
   converse    :: "i => i"
-  relation    :: "i => o"        --\<open>recognizes sets of pairs\<close>
-  "function"  :: "i => o"        --\<open>recognizes functions; can have non-pairs\<close>
+  relation    :: "i => o"        \<comment>\<open>recognizes sets of pairs\<close>
+  "function"  :: "i => o"        \<comment>\<open>recognizes functions; can have non-pairs\<close>
   Lambda      :: "[i, i => i] => i"
   restrict    :: "[i, i] => i"
 
 text \<open>Infixes in order of decreasing precedence\<close>
 consts
 
-  Image       :: "[i, i] => i"    (infixl "``" 90) --\<open>image\<close>
-  vimage      :: "[i, i] => i"    (infixl "-``" 90) --\<open>inverse image\<close>
-  "apply"     :: "[i, i] => i"    (infixl "`" 90) --\<open>function application\<close>
-  "Int"       :: "[i, i] => i"    (infixl "Int" 70) --\<open>binary intersection\<close>
-  "Un"        :: "[i, i] => i"    (infixl "Un" 65) --\<open>binary union\<close>
-  Diff        :: "[i, i] => i"    (infixl "-" 65) --\<open>set difference\<close>
-  Subset      :: "[i, i] => o"    (infixl "<=" 50) --\<open>subset relation\<close>
+  Image       :: "[i, i] => i"    (infixl "``" 90) \<comment>\<open>image\<close>
+  vimage      :: "[i, i] => i"    (infixl "-``" 90) \<comment>\<open>inverse image\<close>
+  "apply"     :: "[i, i] => i"    (infixl "`" 90) \<comment>\<open>function application\<close>
+  "Int"       :: "[i, i] => i"    (infixl "Int" 70) \<comment>\<open>binary intersection\<close>
+  "Un"        :: "[i, i] => i"    (infixl "Un" 65) \<comment>\<open>binary union\<close>
+  Diff        :: "[i, i] => i"    (infixl "-" 65) \<comment>\<open>set difference\<close>
+  Subset      :: "[i, i] => o"    (infixl "<=" 50) \<comment>\<open>subset relation\<close>
 
 axiomatization
-  mem         :: "[i, i] => o"    (infixl ":" 50) --\<open>membership relation\<close>
+  mem         :: "[i, i] => o"    (infixl ":" 50) \<comment>\<open>membership relation\<close>
 
 abbreviation
-  not_mem :: "[i, i] => o"  (infixl "~:" 50)  --\<open>negated membership relation\<close>
+  not_mem :: "[i, i] => o"  (infixl "~:" 50)  \<comment>\<open>negated membership relation\<close>
   where "x ~: y == ~ (x : y)"
 
 abbreviation
-  cart_prod :: "[i, i] => i"    (infixr "*" 80) --\<open>Cartesian product\<close>
+  cart_prod :: "[i, i] => i"    (infixr "*" 80) \<comment>\<open>Cartesian product\<close>
   where "A * B == Sigma(A, %_. B)"
 
 abbreviation
-  function_space :: "[i, i] => i"  (infixr "->" 60) --\<open>function space\<close>
+  function_space :: "[i, i] => i"  (infixr "->" 60) \<comment>\<open>function space\<close>
   where "A -> B == Pi(A, %_. B)"
 
 
@@ -616,8 +616,8 @@
 
 declare Pow_iff [iff]
 
-lemmas Pow_bottom = empty_subsetI [THEN PowI]    --\<open>@{term"0 \<in> Pow(B)"}\<close>
-lemmas Pow_top = subset_refl [THEN PowI]         --\<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>