src/HOL/Real/HahnBanach/document/notation.tex
changeset 7984 86c0cc789f61
parent 7978 1b99ee57d131
child 9278 0b8e87bb91d9
equal deleted inserted replaced
7983:d823fdcc0645 7984:86c0cc789f61
     1 
     1 
     2 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     2 \renewcommand{\isamarkupheader}[1]{\section{#1}}
     3 \newcommand{\isasymlambda}{${\mathtt{\lambda}}$}
       
     4 \newcommand{\isasymprod}{\emph{$\mult$}}
     3 \newcommand{\isasymprod}{\emph{$\mult$}}
     5 \newcommand{\isasymzero}{\emph{$\zero$}}
     4 \newcommand{\isasymzero}{\emph{$\zero$}}
     6 
       
     7 
     5 
     8 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
     6 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
     9 \newcommand{\var}[1]{{?\!#1}}
     7 \newcommand{\var}[1]{{?\!#1}}
    10 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
     8 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
    11 \newcommand{\dsh}{\dshsym}
     9 \newcommand{\dsh}{\dshsym}