--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Thu Nov 05 00:17:13 2015 +0100
@@ -357,10 +357,10 @@
theorem
assumes "\<exists>x. \<forall>y. R x y"
shows "\<forall>y. \<exists>x. R x y"
-proof -- \<open>\<open>\<forall>\<close> introduction\<close>
- obtain x where "\<forall>y. R x y" using \<open>\<exists>x. \<forall>y. R x y\<close> .. -- \<open>\<open>\<exists>\<close> elimination\<close>
- fix y have "R x y" using \<open>\<forall>y. R x y\<close> .. -- \<open>\<open>\<forall>\<close> destruction\<close>
- then show "\<exists>x. R x y" .. -- \<open>\<open>\<exists>\<close> introduction\<close>
+proof \<comment> \<open>\<open>\<forall>\<close> introduction\<close>
+ obtain x where "\<forall>y. R x y" using \<open>\<exists>x. \<forall>y. R x y\<close> .. \<comment> \<open>\<open>\<exists>\<close> elimination\<close>
+ fix y have "R x y" using \<open>\<forall>y. R x y\<close> .. \<comment> \<open>\<open>\<forall>\<close> destruction\<close>
+ then show "\<exists>x. R x y" .. \<comment> \<open>\<open>\<exists>\<close> introduction\<close>
qed