# HG changeset patch
# User wenzelm
# Date 971365964 -7200
# Node ID 2b284ef75049b241dd87770ebd2d5bab683616bb
# Parent  c7c64cd26fc9e22862297bdf34be5ca899e6edfe
tuned syms;

diff -r c7c64cd26fc9 -r 2b284ef75049 doc-src/IsarRef/isar-ref.tex
--- 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}
diff -r c7c64cd26fc9 -r 2b284ef75049 src/HOL/Real/HahnBanach/document/notation.tex
--- 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}}