*** empty log message ***
authornipkow
Thu Jun 16 11:20:52 2005 +0200 (2005-06-16)
changeset 16410d1a436d92d31
parent 16409 a79f8993011b
child 16411 04cc6b4b3439
*** empty log message ***
doc-src/TutorialI/Rules/rules.tex
     1.1 --- a/doc-src/TutorialI/Rules/rules.tex	Thu Jun 16 11:10:51 2005 +0200
     1.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Thu Jun 16 11:20:52 2005 +0200
     1.3 @@ -648,7 +648,7 @@
     1.4  \begin{isabelle}
     1.5  \isacommand{apply} assumption
     1.6  \end{isabelle}
     1.7 -Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information:
     1.8 +Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information that \isa{e} clashes with \isa{c}:
     1.9  \begin{isabelle}
    1.10  Clash: e =/= c\isanewline
    1.11  Clash: == =/= Trueprop