--- a/doc-src/IsarRef/isar-ref.tex Thu Oct 12 17:48:47 2000 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Thu Oct 12 17:52:44 2000 +0200
@@ -11,8 +11,9 @@
\newcommand{\isastyle}{\small\tt\slshape}
\newcommand{\isa}[1]{\emph{\isastyle #1}}
-\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
-\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
\railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
\railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
--- a/src/HOL/Real/HahnBanach/document/notation.tex Thu Oct 12 17:48:47 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Thu Oct 12 17:52:44 2000 +0200
@@ -1,7 +1,7 @@
\renewcommand{\isamarkupheader}[1]{\section{#1}}
-\newcommand{\isasymprod}{\emph{$\mult$}}
-\newcommand{\isasymzero}{\emph{$\zero$}}
+\newcommand{\isasymprod}{\isamath{\mult}}
+\newcommand{\isasymzero}{\isamath{\zero}}
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
\newcommand{\var}[1]{{?\!#1}}