src/HOL/Real/HahnBanach/document/notation.tex
author wenzelm
Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039 a901bafe4578
parent 7984 86c0cc789f61
child 9278 0b8e87bb91d9
permissions -rw-r--r--
Goal: tuned pris;


\renewcommand{\isamarkupheader}[1]{\section{#1}}
\newcommand{\isasymprod}{\emph{$\mult$}}
\newcommand{\isasymzero}{\emph{$\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{\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}{\le}
\newcommand{\Lt}{\lt}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
\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}{\mathord{\mathbf 0}}
\newcommand{\plus}{\mathbin{\mathbf +}}
\newcommand{\minus}{\mathbin{\mathbf -}}
\newcommand{\mult}{\mathbin{\mathbf\odot}}

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