# 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