src/HOL/Real/HahnBanach/document/notation.tex
changeset 10687 c186279eecea
parent 10686 60c795d6bd9e
child 10688 4cf4bbc25267
equal deleted inserted replaced
10686:60c795d6bd9e 10687:c186279eecea
     1 
       
     2 \renewcommand{\isamarkupheader}[1]{\section{#1}}
       
     3 \newcommand{\isasymprod}{\isamath{\mult}}
       
     4 \newcommand{\isasymzero}{\isamath{\zero}}
       
     5 
       
     6 \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
       
     7 \newcommand{\var}[1]{{?\!#1}}
       
     8 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
       
     9 \newcommand{\dsh}{\dshsym}
       
    10 
       
    11 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
       
    12 
       
    13 \newcommand{\skp}{\smallskip}
       
    14 
       
    15 \newcommand{\To}{\to}
       
    16 \newcommand{\dt}{{\mathpunct.}}
       
    17 \newcommand{\Ex}[1]{\exists #1\dt\;}
       
    18 \newcommand{\Forall}{\forall}
       
    19 \newcommand{\All}[1]{\Forall #1\dt\;}
       
    20 \newcommand{\Eq}{\mathbin{\,\equiv\,}}
       
    21 \newcommand{\Impl}{\Rightarrow}
       
    22 \newcommand{\And}{\;\land\;}
       
    23 \newcommand{\Or}{\;\lor\;}
       
    24 \newcommand{\Le}{\leq}
       
    25 \newcommand{\Lt}{\lt}
       
    26 \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
       
    27 %\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
       
    28 \newcommand{\ap}{\mathpalette{\mathbin{}}{\mathbin{}}{\mathbin{}}{\mathbin{}}}
       
    29 \newcommand{\Union}{\bigcup}
       
    30 \newcommand{\Un}{\cup}
       
    31 \newcommand{\Int}{\cap}
       
    32 
       
    33 \newcommand{\norm}[1]{\left\|#1\right\|}
       
    34 \newcommand{\fnorm}[1]{\left\|#1\right\|}
       
    35 \newcommand{\zero}{0}
       
    36 \newcommand{\plus}{\mathbin{\mathbf +}}
       
    37 \newcommand{\minus}{\mathbin{\mathbf -}}
       
    38 \newcommand{\mult}{\cdot}
       
    39 
       
    40 %%% Local Variables:
       
    41 %%% mode: latex
       
    42 %%% TeX-master: "root"
       
    43 %%% End: