diff -r 2e48182cc82c -r cf58b5b794b2 src/HOL/ex/Set_Theory.thy
--- a/src/HOL/ex/Set_Theory.thy	Sat Dec 26 15:44:14 2015 +0100
+++ b/src/HOL/ex/Set_Theory.thy	Sat Dec 26 15:59:27 2015 +0100
@@ -31,14 +31,14 @@
   by blast
 
 
-subsection \<open>Examples for the @{text blast} paper\<close>
+subsection \<open>Examples for the \<open>blast\<close> paper\<close>
 
 lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C)  \<union>  \<Union>(g ` C)"
-  -- \<open>Union-image, called @{text Un_Union_image} in Main HOL\<close>
+  \<comment> \<open>Union-image, called \<open>Un_Union_image\<close> in Main HOL\<close>
   by blast
 
 lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
-  -- \<open>Inter-image, called @{text Int_Inter_image} in Main HOL\<close>
+  \<comment> \<open>Inter-image, called \<open>Int_Inter_image\<close> in Main HOL\<close>
   by blast
 
 lemma singleton_example_1:
@@ -47,30 +47,30 @@
 
 lemma singleton_example_2:
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-  -- \<open>Variant of the problem above.\<close>
+  \<comment> \<open>Variant of the problem above.\<close>
   by blast
 
 lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
-  -- \<open>A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail.\<close>
+  \<comment> \<open>A unique fixpoint theorem --- \<open>fast\<close>/\<open>best\<close>/\<open>meson\<close> all fail.\<close>
   by metis
 
 
 subsection \<open>Cantor's Theorem: There is no surjection from a set to its powerset\<close>
 
 lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
-  -- \<open>Requires best-first search because it is undirectional.\<close>
+  \<comment> \<open>Requires best-first search because it is undirectional.\<close>
   by best
 
 schematic_goal "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
-  -- \<open>This form displays the diagonal term.\<close>
+  \<comment> \<open>This form displays the diagonal term.\<close>
   by best
 
 schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-  -- \<open>This form exploits the set constructs.\<close>
+  \<comment> \<open>This form exploits the set constructs.\<close>
   by (rule notI, erule rangeE, best)
 
 schematic_goal "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
-  -- \<open>Or just this!\<close>
+  \<comment> \<open>Or just this!\<close>
   by best
 
 
@@ -102,7 +102,7 @@
     \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
   apply (rule decomposition [where f=f and g=g, THEN exE])
   apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI) 
-    --\<open>The term above can be synthesized by a sufficiently detailed proof.\<close>
+    \<comment>\<open>The term above can be synthesized by a sufficiently detailed proof.\<close>
   apply (rule bij_if_then_else)
      apply (rule_tac [4] refl)
     apply (rule_tac [2] inj_on_inv_into)
@@ -166,38 +166,38 @@
 \<close>
 
 lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
-  -- \<open>Example 1, page 295.\<close>
+  \<comment> \<open>Example 1, page 295.\<close>
   by force
 
 lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
-  -- \<open>Example 2.\<close>
+  \<comment> \<open>Example 2.\<close>
   by force
 
 lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
-  -- \<open>Example 3.\<close>
+  \<comment> \<open>Example 3.\<close>
   by force
 
 lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
-  -- \<open>Example 4.\<close>
-  by auto --\<open>slow\<close>
+  \<comment> \<open>Example 4.\<close>
+  by auto \<comment>\<open>slow\<close>
 
 lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
-  -- \<open>Example 5, page 298.\<close>
+  \<comment> \<open>Example 5, page 298.\<close>
   by force
 
 lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
-  -- \<open>Example 6.\<close>
+  \<comment> \<open>Example 6.\<close>
   by force
 
 lemma "\<exists>A. a \<notin> A"
-  -- \<open>Example 7.\<close>
+  \<comment> \<open>Example 7.\<close>
   by force
 
 lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
     \<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. abs y \<notin> A))"
-  -- \<open>Example 8 needs a small hint.\<close>
+  \<comment> \<open>Example 8 needs a small hint.\<close>
   by force
-    -- \<open>not @{text blast}, which can't simplify @{text "-2 < 0"}\<close>
+    \<comment> \<open>not \<open>blast\<close>, which can't simplify \<open>-2 < 0\<close>\<close>
 
 text \<open>Example 9 omitted (requires the reals).\<close>
 
@@ -205,19 +205,19 @@
 
 lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
   P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
-  -- \<open>Example 11: needs a hint.\<close>
+  \<comment> \<open>Example 11: needs a hint.\<close>
 by(metis nat.induct)
 
 lemma
   "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
     \<and> P n \<longrightarrow> P m"
-  -- \<open>Example 12.\<close>
+  \<comment> \<open>Example 12.\<close>
   by auto
 
 lemma
   "(\<forall>x. (\<exists>u. x = 2 * u) = (\<not> (\<exists>v. Suc x = 2 * v))) \<longrightarrow>
     (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
-  -- \<open>Example EO1: typo in article, and with the obvious fix it seems
+  \<comment> \<open>Example EO1: typo in article, and with the obvious fix it seems
       to require arithmetic reasoning.\<close>
   apply clarify
   apply (rule_tac x = "{x. \<exists>u. x = 2 * u}" in exI, auto)