--- a/doc-src/TutorialI/Rules/rules.tex Thu Jun 16 11:10:51 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Jun 16 11:20:52 2005 +0200
@@ -648,7 +648,7 @@
\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