diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/let_rewr.tex
--- a/doc-src/TutorialI/Misc/document/let_rewr.tex	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/let_rewr.tex	Sun Aug 06 15:26:53 2000 +0200
@@ -1,11 +1,11 @@
 \begin{isabelle}%
-\isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline
-\isacommand{by}(simp~add:~Let\_def)%
+\isacommand{lemma}\ {"}(let\ xs\ =\ []\ in\ xs@ys@xs)\ =\ ys{"}\isanewline
+\isacommand{by}(simp\ add:\ Let\_def)%
 \begin{isamarkuptext}%
 If, in a particular context, there is no danger of a combinatorial explosion
 of nested \isa{let}s one could even add \isa{Let_def} permanently:%
 \end{isamarkuptext}%
-\isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}%
+\isacommand{lemmas}\ [simp]\ =\ Let\_def\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"