1.1 --- a/doc-src/IsarRef/isar-ref.tex	Thu Oct 12 17:48:47 2000 +0200
     1.2 +++ b/doc-src/IsarRef/isar-ref.tex	Thu Oct 12 17:52:44 2000 +0200
     1.3 @@ -11,8 +11,9 @@
     1.4  
     1.5  \newcommand{\isastyle}{\small\tt\slshape}
     1.6  \newcommand{\isa}[1]{\emph{\isastyle #1}}
     1.7 -\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
     1.8 -\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
     1.9 +\newcommand{\isamath}[1]{\emph{$#1$}}
    1.10 +\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
    1.11 +\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
    1.12  
    1.13  \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
    1.14  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}

     2.1 --- a/src/HOL/Real/HahnBanach/document/notation.tex	Thu Oct 12 17:48:47 2000 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/document/notation.tex	Thu Oct 12 17:52:44 2000 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  
     2.5  \renewcommand{\isamarkupheader}[1]{\section{#1}}
     2.6 -\newcommand{\isasymprod}{\emph{$\mult$}}
     2.7 -\newcommand{\isasymzero}{\emph{$\zero$}}
     2.8 +\newcommand{\isasymprod}{\isamath{\mult}}
     2.9 +\newcommand{\isasymzero}{\isamath{\zero}}
    2.10  
    2.11  \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    2.12  \newcommand{\var}[1]{{?\!#1}}