src/HOL/Real/HahnBanach/document/notation.tex
changeset 10208 2b284ef75049
parent 9394 1ff8a6234c6a
equal deleted inserted replaced
10207:c7c64cd26fc9 10208:2b284ef75049
     1 
     1 
     2 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     2 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     3 \newcommand{\isasymprod}{\emph{$\mult$}}
     3 \newcommand{\isasymprod}{\isamath{\mult}}
     4 \newcommand{\isasymzero}{\emph{$\zero$}}
     4 \newcommand{\isasymzero}{\isamath{\zero}}
     5 
     5 
     6 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
     6 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
     7 \newcommand{\var}[1]{{?\!#1}}
     7 \newcommand{\var}[1]{{?\!#1}}
     8 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
     8 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
     9 \newcommand{\dsh}{\dshsym}
     9 \newcommand{\dsh}{\dshsym}