--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Thu Aug 17 21:07:25 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Fri Aug 18 10:34:08 2000 +0200
@@ -10,7 +10,7 @@
\noindent
Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
sequence of methods. Assuming that the simplification rule
-\isa{(rev\ xs\ =\ [])\ =\ (xs\ =\ [])}
+\isa{(rev\ \mbox{xs}\ =\ [])\ =\ (\mbox{xs}\ =\ [])}
is present as well,%
\end{isamarkuptext}%
\isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ \#\ tl(rev\ xs)\ =\ rev\ xs{"}%