1.1 --- a/src/HOL/Real/HahnBanach/document/notation.tex	Thu Oct 12 17:48:47 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/document/notation.tex	Thu Oct 12 17:52:44 2000 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  
     1.5  \renewcommand{\isamarkupheader}[1]{\section{#1}}
     1.6 -\newcommand{\isasymprod}{\emph{$\mult$}}
     1.7 -\newcommand{\isasymzero}{\emph{$\zero$}}
     1.8 +\newcommand{\isasymprod}{\isamath{\mult}}
     1.9 +\newcommand{\isasymzero}{\isamath{\zero}}
    1.10  
    1.11  \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    1.12  \newcommand{\var}[1]{{?\!#1}}