diff -r 634cd44bb1d3 -r c49a8ebd30cc src/Doc/Eisbach/Manual.thy
--- a/src/Doc/Eisbach/Manual.thy	Thu Nov 05 00:02:30 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy	Thu Nov 05 00:17:13 2015 +0100
@@ -249,16 +249,16 @@
 \<close>
 
     lemmas [intros] =
-      conjI  --  \<open>@{thm conjI}\<close>
-      impI  --  \<open>@{thm impI}\<close>
-      disjCI  --  \<open>@{thm disjCI}\<close>
-      iffI  --  \<open>@{thm iffI}\<close>
-      notI  --  \<open>@{thm notI}\<close>
+      conjI  \<comment>  \<open>@{thm conjI}\<close>
+      impI  \<comment>  \<open>@{thm impI}\<close>
+      disjCI  \<comment>  \<open>@{thm disjCI}\<close>
+      iffI  \<comment>  \<open>@{thm iffI}\<close>
+      notI  \<comment>  \<open>@{thm notI}\<close>
 
     lemmas [elims] =
-      impCE  --  \<open>@{thm impCE}\<close>
-      conjE  --  \<open>@{thm conjE}\<close>
-      disjE  --  \<open>@{thm disjE}\<close>
+      impCE  \<comment>  \<open>@{thm impCE}\<close>
+      conjE  \<comment>  \<open>@{thm conjE}\<close>
+      disjE  \<comment>  \<open>@{thm disjE}\<close>
 
     lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C"
       by prop_solver