src/FOL/ex/Classical.thy

   "(\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> (\<forall>z. p(z,x) \<longleftrightarrow> p(z,y)))
     \<longrightarrow> (\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> q(y,x))"
   by blast
 
 text \<open>
-  Other proofs: Can use @{text auto}, which cheats by using rewriting!
-  @{text Deepen_tac} alone requires 253 secs.  Or
-  @{text \<open>by (mini_tac 1 THEN Deepen_tac 5 1)\<close>}.
+  Other proofs: Can use \<open>auto\<close>, which cheats by using rewriting!
+  \<open>Deepen_tac\<close> alone requires 253 secs.  Or
+  \<open>by (mini_tac 1 THEN Deepen_tac 5 1)\<close>.
 \<close>
 
 text\<open>44\<close>
 lemma
   "(\<forall>x. f(x) \<longrightarrow> (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and>

 lemma
   "(\<exists>x y::'a. \<forall>z. z = x \<or> z = y) \<and> P(a) \<and> P(b) \<and> a \<noteq> b \<longrightarrow> (\<forall>u::'a. P(u))"
   apply safe
   apply (rule_tac x = a in allE, assumption)
   apply (rule_tac x = b in allE, assumption)
-  apply fast  -- \<open>blast's treatment of equality can't do it\<close>
+  apply fast  \<comment> \<open>blast's treatment of equality can't do it\<close>
   done
 
 text\<open>50. (What has this to do with equality?)\<close>
 lemma "(\<forall>x. P(a,x) \<or> (\<forall>y. P(x,y))) \<longrightarrow> (\<exists>x. \<forall>y. P(x,y))"
   by blast

    (hates(agatha,agatha) \<and> hates(agatha,charles)) \<and>
    (\<forall>x. lives(x) \<and> \<not> richer(x,agatha) \<longrightarrow> hates(butler,x)) \<and>
    (\<forall>x. hates(agatha,x) \<longrightarrow> hates(butler,x)) \<and>
    (\<forall>x. \<not> hates(x,agatha) \<or> \<not> hates(x,butler) \<or> \<not> hates(x,charles)) \<longrightarrow>
     killed(?who,agatha)"
-  by fast  -- \<open>MUCH faster than blast\<close>
+  by fast  \<comment> \<open>MUCH faster than blast\<close>
 
 
 text\<open>56\<close>
 lemma "(\<forall>x. (\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
   by blast

       (\<exists>v. C(v) \<and>
             (\<forall>y. ((C(y) \<and> Q(w,y,y)) \<and> OO(w,g) \<longrightarrow> \<not> P(v,y)) \<and>
                     ((C(y) \<and> Q(w,y,y)) \<and> OO(w,b) \<longrightarrow> P(v,y) \<and> OO(v,b)))))
      \<longrightarrow> \<not> (\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z))))"
   by (blast 12)
-    -- \<open>Needed because the search for depths below 12 is very slow.\<close>
+    \<comment> \<open>Needed because the search for depths below 12 is very slow.\<close>
 
 
 text \<open>
   Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1),
   p. 105.