# HG changeset patch
# User nipkow
# Date 1118913652 -7200
# Node ID d1a436d92d3176aeadcd5669e0cde9701a66196f
# Parent  a79f8993011b90d0bc933c135973eb386f9d7b27
*** empty log message ***

diff -r a79f8993011b -r d1a436d92d31 doc-src/TutorialI/Rules/rules.tex
--- 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