src/HOL/Real/HahnBanach/document/notation.tex

tuned syms;

\renewcommand{\isamarkupheader}[1]{\section{#1}}
\newcommand{\isasymprod}{\isamath{\mult}}
\newcommand{\isasymzero}{\isamath{\zero}}

\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
\newcommand{\var}[1]{{?\!#1}}
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
\newcommand{\dsh}{\dshsym}

\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}

\newcommand{\skp}{\smallskip}

\newcommand{\To}{\to}
\newcommand{\dt}{{\mathpunct.}}
\newcommand{\Ex}[1]{\exists #1\dt\;}
\newcommand{\Forall}{\forall}
\newcommand{\All}[1]{\Forall #1\dt\;}
\newcommand{\Eq}{\mathbin{\,\equiv\,}}
\newcommand{\Impl}{\Rightarrow}
\newcommand{\And}{\;\land\;}
\newcommand{\Or}{\;\lor\;}
\newcommand{\Le}{\leq}
\newcommand{\Lt}{\lt}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
%\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
\newcommand{\ap}{\mathpalette{\mathbin{}}{\mathbin{}}{\mathbin{}}{\mathbin{}}}
\newcommand{\Union}{\bigcup}
\newcommand{\Un}{\cup}
\newcommand{\Int}{\cap}

\newcommand{\norm}[1]{\left\|#1\right\|}
\newcommand{\fnorm}[1]{\left\|#1\right\|}
\newcommand{\zero}{0}
\newcommand{\plus}{\mathbin{\mathbf +}}
\newcommand{\minus}{\mathbin{\mathbf -}}
\newcommand{\mult}{\cdot}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: