diff -r 2c208c98f541 -r 1b2d4f995b13 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Mon Aug 21 19:03:58 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Mon Aug 21 19:17:07 2000 +0200
@@ -8,34 +8,64 @@
 
 % isabelle environments
 
-\newcommand{\isabellestyle}{\small\tt\slshape}
+\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastyletext}{\normalsize\rm}
+\newcommand{\isastyletxt}{\rm}
+\newcommand{\isastylecmt}{\rm}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
+
 \newenvironment{isabelle}{%
 \isa@parindent\parindent\parindent0pt%
 \isa@parskip\parskip\parskip0pt%
-\isabellestyle}{}
+\isastyle}{}
 
-\newcommand{\isa}[1]{\emph{\isabellestyle #1}}
-
-\newenvironment{isabellequote}%
-{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}
+\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
 
 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
+\newcommand{\isadigit}[1]{#1}
 
-\chardef\isabraceleft=`\{
-\chardef\isabraceright=`\}
-\chardef\isatilde=`\~
-\chardef\isacircum=`\^
-\chardef\isabackslash=`\\
+\chardef\isacharbang=`\!
+\chardef\isachardoublequote=`\"
+\chardef\isacharhash=`\#
+\chardef\isachardollar=`\$
+\chardef\isacharpercent=`\%
+\chardef\isacharampersand=`\&
+\chardef\isacharprime=`\'
+\chardef\isacharparenleft=`\(
+\chardef\isacharparenright=`\)
+\chardef\isacharasterisk=`\*
+\chardef\isacharplus=`\+
+\chardef\isacharcomma=`\,
+\chardef\isacharminus=`\-
+\chardef\isachardot=`\.
+\chardef\isacharslash=`\/
+\chardef\isacharcolon=`\:
+\chardef\isacharsemicolon=`\;
+\chardef\isacharless=`\<
+\chardef\isacharequal=`\=
+\chardef\isachargreater=`\>
+\chardef\isacharquery=`\?
+\chardef\isacharat=`\@
+\chardef\isacharbrackleft=`\[
+\chardef\isacharbackslash=`\\
+\chardef\isacharbrackright=`\]
+\chardef\isacharcircum=`\^
+\chardef\isacharunderscore=`\_
+\chardef\isacharbackquote=`\`
+\chardef\isacharbraceleft=`\{
+\chardef\isacharbar=`\|
+\chardef\isacharbraceright=`\}
+\chardef\isachartilde=`\~
 
 
 % keyword and section markup
 
-\newcommand{\isacommand}[1]{\emph{\bf #1}}
-\newcommand{\isakeyword}[1]{\emph{\bf #1}}
-\newcommand{\isabeginblock}{\isakeyword{\{}}
-\newcommand{\isaendblock}{\isakeyword{\}}}
+\newcommand{\isakeyword}[1]
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{-}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
 
 \newcommand{\isamarkupheader}[1]{\section{#1}}
 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
@@ -47,6 +77,48 @@
 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
 
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
-\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
-\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}
+\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% alternative styles -- default is "tt"
+
+\newcommand{\isabellestyle}{}
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestyleit}{%
+\renewcommand{\isastyle}{\small\it}%
+\renewcommand{\isastyleminor}{\it}%
+%\renewcommand{\isadigit}[1]{\emph{$##1$}}
+\renewcommand{\isacharbang}{\emph{$!$}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharhash}{\emph{$\#$}}%
+\renewcommand{\isachardollar}{\emph{$\$$}}%
+\renewcommand{\isacharpercent}{\emph{$\%$}}%
+\renewcommand{\isacharampersand}{\emph{$\&$}}%
+\renewcommand{\isacharprime}{$\mskip2mu{'}\mskip-2mu$}%
+\renewcommand{\isacharparenleft}{\emph{$($}}%
+\renewcommand{\isacharparenright}{\emph{$)$}}%
+\renewcommand{\isacharasterisk}{\emph{$*$}}%
+\renewcommand{\isacharplus}{\emph{$+$}}%
+\renewcommand{\isacharcomma}{\emph{$\mathord,$}}%
+\renewcommand{\isacharminus}{\emph{$-$}}%
+\renewcommand{\isachardot}{\emph{$\mathord.$}}%
+\renewcommand{\isacharslash}{\emph{$/$}}%
+\renewcommand{\isacharcolon}{\emph{$\mathord:$}}%
+\renewcommand{\isacharsemicolon}{\emph{$\mathord;$}}%
+\renewcommand{\isacharless}{\emph{$<$}}%
+\renewcommand{\isacharequal}{\emph{$=$}}%
+\renewcommand{\isachargreater}{\emph{$>$}}%
+%\renewcommand{\isacharquery}{\emph{$\mathord?$}}%
+\renewcommand{\isacharat}{\emph{$@$}}%
+\renewcommand{\isacharbrackleft}{\emph{$[$}}%
+\renewcommand{\isacharbrackright}{\emph{$]$}}%
+\renewcommand{\isacharunderscore}{-}%
+\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
+\renewcommand{\isacharbar}{\emph{$\mid$}}%
+\renewcommand{\isacharbraceright}{\emph{$\}$}}%
+}
+
+\newcommand{\isabellestylesl}{\isabellestyleit\renewcommand{\isastyle}{\small\slshape}}