--- 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