doc-src/TutorialI/Rules/rules.tex

 \end{isabelle}
 The \isa{assumption} method having failed, we try again with the flag set:
 \begin{isabelle}
 \isacommand{apply} assumption
 \end{isabelle}
-Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information:
+Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information that \isa{e} clashes with \isa{c}:
 \begin{isabelle}
 Clash: e =/= c\isanewline
 Clash: == =/= Trueprop
 \end{isabelle}