--- 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
--- a/doc-src/iman.sty Thu Nov 20 11:03:53 1997 +0100
+++ b/doc-src/iman.sty Thu Nov 20 11:53:51 1997 +0100
@@ -142,8 +142,7 @@
\chardef\ttlbrace=`\{ % A left brace for \tt font
\chardef\ttrbrace=`\} % A right brace for \tt font
-\newfont{\sltt}{cmsltt10} %% for output from terminal sessions
-\newcommand\out{\ \sltt}
+\newcommand\out{\ \ttfamily\slshape} %% for output from terminal sessions
% The mathcodes for the letters A, ..., Z, a, ..., z are changed to
% generate text italic rather than math italic by default. This makes