diff -r 39ffdb8cab03 -r 87ba969d069c doc-src/TutorialI/isabellesym.sty
--- 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$}}