--- a/doc-src/TutorialI/isabelle.sty Sat Sep 02 21:56:24 2000 +0200
+++ b/doc-src/TutorialI/isabelle.sty Sat Sep 02 22:19:03 2000 +0200
@@ -95,8 +95,7 @@
\newcommand{\isabellestyleit}{%
\renewcommand{\isastyle}{\small\it}%
\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isakeywordcharunderscore}{-}%
-%\renewcommand{\isadigit}[1]{\emph{$##1$}}
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
\renewcommand{\isacharbang}{\emph{$!$}}%
\renewcommand{\isachardoublequote}{}%
\renewcommand{\isacharhash}{\emph{$\#$}}%
@@ -117,11 +116,10 @@
\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{\isacharunderscore}{\mbox{-}}%
\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
\renewcommand{\isacharbar}{\emph{$\mid$}}%
\renewcommand{\isacharbraceright}{\emph{$\}$}}%