updated;

--- 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{$\}$}}%

--- a/doc-src/TutorialI/isabellesym.sty	Sat Sep 02 21:56:24 2000 +0200
+++ b/doc-src/TutorialI/isabellesym.sty	Sat Sep 02 22:19:03 2000 +0200
@@ -1,15 +1,14 @@
 %%
 %% $Id$
 %%
-%% definitions of many Isabelle symbols
+%% definitions of standard Isabelle symbols
 %%
 
 \usepackage{latexsym}
 %\usepackage{amssymb}
 %\usepackage[latin1]{inputenc}
 
-\newcommand{\bigsqcap}{\overline{|\,\,|}}  %just a hack
-%\def\textbrokenbar??? etc
+\newcommand{\bigsqcap}{\overline{|\,\,|}}  %an approximation ...
 
 \newcommand{\isasymspacespace}{~~}
 \newcommand{\isasymGamma}{$\Gamma$}
@@ -173,15 +172,15 @@
 \newcommand{\isasymemptyset}{\emph{$\emptyset$}}
 \newcommand{\isasymangle}{\emph{$\angle$}}
 \newcommand{\isasymnabla}{\emph{$\nabla$}}
-\newcommand{\isasymProd}{\emph{$\prod$}}
+\newcommand{\isasymProd}{\emph{$\prod\,$}}
 \newcommand{\isasymLeftrightarrow}{\emph{$\Leftrightarrow$}}
 \newcommand{\isasymUparrow}{\emph{$\Uparrow$}}
 \newcommand{\isasymDownarrow}{\emph{$\Downarrow$}}
 \newcommand{\isasymlozenge}{\emph{$\lozenge$}}
 \newcommand{\isasymlangle}{\emph{$\langle$}}
 \newcommand{\isasymrangle}{\emph{$\rangle$}}
-\newcommand{\isasymSum}{\emph{$\sum$}}
-\newcommand{\isasymintegral}{\emph{$\int$}}
+\newcommand{\isasymSum}{\emph{$\sum\,$}}
+\newcommand{\isasymintegral}{\emph{$\int\,$}}
 \newcommand{\isasymdagger}{\emph{$\dagger$}}
 \newcommand{\isasymsharp}{\emph{$\sharp$}}
 \newcommand{\isasymstar}{\emph{$\star$}}
@@ -232,7 +231,7 @@
 \newcommand{\isasymreal}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{R}$}}
 \newcommand{\isasymint}{\emph{$\mathsf{Z}\mkern-7.5mu\mathsf{Z}$}}
 
-%requires amssymb
+%require amssymb:
 \newcommand{\isasymlesssim}{\emph{$\lesssim$}}
 \newcommand{\isasymgreatersim}{\emph{$\gtrsim$}}
 \newcommand{\isasymlessapprox}{\emph{$\lessapprox$}}