# HG changeset patch
# User paulson
# Date 880023231 -3600
# Node ID f50dace8be9fa71f7440d82c7602bbd573ab0c3f
# Parent  d7b8dd96051447551a9d5bd792369d844a9d7f9b
New, higher-level definition of \\out macro

diff -r d7b8dd960514 -r f50dace8be9f doc-src/Intro/getting.tex
--- 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
diff -r d7b8dd960514 -r f50dace8be9f doc-src/iman.sty
--- 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