--- a/doc-src/Intro/getting.tex Thu Nov 20 11:03:53 1997 +0100
+++ b/doc-src/Intro/getting.tex Thu Nov 20 11:53:51 1997 +0100
@@ -236,7 +236,7 @@
{\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm}
\end{ttbox}
User input appears in {\footnotesize\tt typewriter characters}, and output
-appears in {\sltt slanted typewriter characters}. \ML's response {\out val
+appears in{\out slanted typewriter characters}. \ML's response {\out val
}~\ldots{} is compiler-dependent and will sometimes be suppressed. This
session illustrates two formats for the display of theorems. Isabelle's
top-level displays theorems as \ML{} values, enclosed in quotes. Printing