src/HOL/Real/HahnBanach/document/notation.tex
author fleuriot
Thu, 01 Jun 2000 11:22:27 +0200
changeset 9013 9dd0274f76af
parent 7984 86c0cc789f61
child 9278 0b8e87bb91d9
permissions -rw-r--r--
Updated files to remove 0r and 1r from theorems in descendant theories of RealBin. Some new theorems added.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
     1
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
     2
\renewcommand{\isamarkupheader}[1]{\section{#1}}
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
     3
\newcommand{\isasymprod}{\emph{$\mult$}}
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
     4
\newcommand{\isasymzero}{\emph{$\zero$}}
7927
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
     5
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
     6
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
     7
\newcommand{\var}[1]{{?\!#1}}
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
     8
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
     9
\newcommand{\dsh}{\dshsym}
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
    10
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    11
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    12
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
    13
\newcommand{\To}{\to}
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
    14
\newcommand{\dt}{{\mathpunct.}}
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
    15
\newcommand{\Ex}[1]{\exists #1\dt\;}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    16
\newcommand{\Forall}{\forall}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    17
\newcommand{\All}[1]{\Forall #1\dt\;}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    18
\newcommand{\Eq}{\mathbin{\,\equiv\,}}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    19
\newcommand{\Impl}{\Rightarrow}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    20
\newcommand{\And}{\;\land\;}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    21
\newcommand{\Or}{\;\lor\;}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    22
\newcommand{\Le}{\le}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    23
\newcommand{\Lt}{\lt}
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    24
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
    25
\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
7927
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    26
\newcommand{\Union}{\bigcup}
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
    27
\newcommand{\Un}{\cup}
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
    28
\newcommand{\Int}{\cap}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    29
7927
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    30
\newcommand{\norm}[1]{\left\|#1\right\|}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    31
\newcommand{\fnorm}[1]{\left\|#1\right\|}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    32
\newcommand{\zero}{\mathord{\mathbf 0}}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    33
\newcommand{\plus}{\mathbin{\mathbf +}}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    34
\newcommand{\minus}{\mathbin{\mathbf -}}
b50446a33c16 update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    35
\newcommand{\mult}{\mathbin{\mathbf\odot}}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    36
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
    37
%%% Local Variables:
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
    38
%%% mode: latex
fd019ac3485f update from Gertrud;
wenzelm
parents: 7792
diff changeset
    39
%%% TeX-master: "root"
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7927
diff changeset
    40
%%% End: