doc-src/AxClass/generated/isabellesym.sty
author wenzelm
Sun, 17 Sep 2000 13:51:37 +0200
changeset 10005 8cd7ef5b8f9d
parent 9845 1206c7615a47
child 10207 c7c64cd26fc9
permissions -rw-r--r--
updated;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     1
%%
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     2
%% $Id$
9845
1206c7615a47 updated;
wenzelm
parents: 9767
diff changeset
     3
%% Author: Markus Wenzel, TU Muenchen
1206c7615a47 updated;
wenzelm
parents: 9767
diff changeset
     4
%% License: GPL (GNU GENERAL PUBLIC LICENSE)
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     5
%%
9767
dc2ee9b2e065 updated;
wenzelm
parents: 9694
diff changeset
     6
%% definitions of standard Isabelle symbols
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     7
%%
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
     8
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
     9
% Required packages for unusual symbols -- see below for details.
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    10
%\usepackage{latexsym}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
    11
%\usepackage{amssymb}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    12
%\usepackage[english]{babel}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    13
%\usepackage[latin1]{inputenc}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    14
%\usepackage[only,bigsqcap]{stmaryrd}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    15
%\usepackage{wasysym}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    16
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    17
% Note: \emph is important for proper spacing in fake math mode, it
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    18
% automatically inserts italic corrections around symbols wherever
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    19
% appropriate.
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    20
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    21
\newcommand{\isasymspacespace}{~~}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    22
\newcommand{\isasymGamma}{$\Gamma$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    23
\newcommand{\isasymDelta}{$\Delta$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    24
\newcommand{\isasymTheta}{$\Theta$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    25
\newcommand{\isasymLambda}{$\Lambda$}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
    26
\newcommand{\isasymXi}{$\Xi$}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    27
\newcommand{\isasymPi}{$\Pi$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    28
\newcommand{\isasymSigma}{$\Sigma$}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
    29
\newcommand{\isasymUpsilon}{$\Upsilon$}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    30
\newcommand{\isasymPhi}{$\Phi$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    31
\newcommand{\isasymPsi}{$\Psi$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    32
\newcommand{\isasymOmega}{$\Omega$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    33
\newcommand{\isasymalpha}{$\alpha$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    34
\newcommand{\isasymbeta}{$\beta$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    35
\newcommand{\isasymgamma}{$\gamma$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    36
\newcommand{\isasymdelta}{$\delta$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    37
\newcommand{\isasymepsilon}{$\varepsilon$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    38
\newcommand{\isasymzeta}{$\zeta$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    39
\newcommand{\isasymeta}{$\eta$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    40
\newcommand{\isasymtheta}{$\vartheta$}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
    41
\newcommand{\isasymiota}{$\iota$}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    42
\newcommand{\isasymkappa}{$\kappa$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    43
\newcommand{\isasymlambda}{$\lambda$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    44
\newcommand{\isasymmu}{$\mu$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    45
\newcommand{\isasymnu}{$\nu$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    46
\newcommand{\isasymxi}{$\xi$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    47
\newcommand{\isasympi}{$\pi$}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
    48
\newcommand{\isasymrho}{$\varrho$}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    49
\newcommand{\isasymsigma}{$\sigma$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    50
\newcommand{\isasymtau}{$\tau$}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
    51
\newcommand{\isasymupsilon}{$\upsilon$}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    52
\newcommand{\isasymphi}{$\varphi$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    53
\newcommand{\isasymchi}{$\chi$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    54
\newcommand{\isasympsi}{$\psi$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    55
\newcommand{\isasymomega}{$\omega$}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    56
\newcommand{\isasymnot}{\emph{$\neg$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    57
\newcommand{\isasymand}{\emph{$\wedge$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    58
\newcommand{\isasymor}{\emph{$\vee$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    59
\newcommand{\isasymforall}{\emph{$\forall\,$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    60
\newcommand{\isasymexists}{\emph{$\exists\,$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    61
\newcommand{\isasymAnd}{\emph{$\bigwedge\,$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    62
\newcommand{\isasymlceil}{\emph{$\lceil$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    63
\newcommand{\isasymrceil}{\emph{$\rceil$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    64
\newcommand{\isasymlfloor}{\emph{$\lfloor$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    65
\newcommand{\isasymrfloor}{\emph{$\rfloor$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    66
\newcommand{\isasymturnstile}{\emph{$\vdash$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    67
\newcommand{\isasymTurnstile}{\emph{$\models$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    68
\newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    69
\newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    70
\newcommand{\isasymcdot}{\emph{$\cdot$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    71
\newcommand{\isasymin}{\emph{$\in$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    72
\newcommand{\isasymsubseteq}{\emph{$\subseteq$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    73
\newcommand{\isasyminter}{\emph{$\cap$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    74
\newcommand{\isasymunion}{\emph{$\cup$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    75
\newcommand{\isasymInter}{\emph{$\bigcap\,$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    76
\newcommand{\isasymUnion}{\emph{$\bigcup\,$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    77
\newcommand{\isasymsqinter}{\emph{$\sqcap$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    78
\newcommand{\isasymsqunion}{\emph{$\sqcup$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    79
\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}}  %requires stmaryrd
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    80
\newcommand{\isasymSqunion}{\emph{$\bigsqcup\,$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    81
\newcommand{\isasymbottom}{\emph{$\bot$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    82
\newcommand{\isasymdoteq}{\emph{$\doteq$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    83
\newcommand{\isasymequiv}{\emph{$\equiv$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    84
\newcommand{\isasymnoteq}{\emph{$\not=$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    85
\newcommand{\isasymsqsubset}{\emph{$\sqsubset$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    86
\newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    87
\newcommand{\isasymprec}{\emph{$\prec$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    88
\newcommand{\isasympreceq}{\emph{$\preceq$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    89
\newcommand{\isasymsucc}{\emph{$\succ$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    90
\newcommand{\isasymapprox}{\emph{$\approx$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    91
\newcommand{\isasymsim}{\emph{$\sim$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    92
\newcommand{\isasymsimeq}{\emph{$\simeq$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    93
\newcommand{\isasymle}{\emph{$\le$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    94
\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    95
\newcommand{\isasymleftarrow}{\emph{$\leftarrow$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    96
\newcommand{\isasymmidarrow}{\emph{$\relbar$}}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    97
\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
    98
\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
    99
\newcommand{\isasymMidarrow}{\emph{$\Relbar$}}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   100
\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   101
\newcommand{\isasymfrown}{\emph{$\frown$}}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   102
\newcommand{\isasymmapsto}{\emph{$\mapsto$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   103
\newcommand{\isasymleadsto}{\emph{$\leadsto$}}  %requires latexsym
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   104
\newcommand{\isasymup}{\emph{$\uparrow$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   105
\newcommand{\isasymdown}{\emph{$\downarrow$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   106
\newcommand{\isasymnotin}{\emph{$\notin$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   107
\newcommand{\isasymtimes}{\emph{$\times$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   108
\newcommand{\isasymoplus}{\emph{$\oplus$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   109
\newcommand{\isasymominus}{\emph{$\ominus$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   110
\newcommand{\isasymotimes}{\emph{$\otimes$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   111
\newcommand{\isasymoslash}{\emph{$\oslash$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   112
\newcommand{\isasymsubset}{\emph{$\subset$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   113
\newcommand{\isasyminfinity}{\emph{$\infty$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   114
\newcommand{\isasymbox}{\emph{$\Box$}}  %requires latexsym
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   115
\newcommand{\isasymdiamond}{\emph{$\Diamond$}}  %requires latexsym
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   116
\newcommand{\isasymcirc}{\emph{$\circ$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   117
\newcommand{\isasymbullet}{\emph{$\bullet$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   118
\newcommand{\isasymparallel}{\emph{$\parallel$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   119
\newcommand{\isasymsurd}{\emph{$\surd$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   120
\newcommand{\isasymcopyright}{\emph{\copyright}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   121
\newcommand{\isasymplusminus}{\emph{$\pm$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   122
\newcommand{\isasymdiv}{\emph{$\div$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   123
\newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   124
\newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   125
\newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   126
\newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   127
\newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   128
\newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   129
\newcommand{\isasymbar}{\emph{$\mid$}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   130
\newcommand{\isasymhyphen}{\emph{\rm-}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   131
\newcommand{\isasymmacron}{\emph{\rm\=\relax}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   132
\newcommand{\isasymexclamdown}{\emph{\rm\textexclamdown}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   133
\newcommand{\isasymquestiondown}{\emph{\rm\textquestiondown}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   134
\newcommand{\isasymguillemotleft}{\emph{\flqq}}  %requires babel
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   135
\newcommand{\isasymguillemotright}{\emph{\frqq}}  %requires babel
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   136
\newcommand{\isasymdegree}{\emph{\rm\textdegree}}  %requires latin1
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   137
\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}}  %requires latin1
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   138
\newcommand{\isasymonequarter}{\emph{\rm\textonequarter}}  %requires latin1
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   139
\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}}  %requires latin1
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   140
\newcommand{\isasymonehalf}{\emph{\rm\textonehalf}}  %requires latin1
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   141
\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}}  %requires latin1
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   142
\newcommand{\isasymthreequarters}{\emph{\rm\textthreequarters}}  %requires latin1
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   143
\newcommand{\isasymparagraph}{\emph{\P}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   144
\newcommand{\isasymregistered}{\emph{\rm\textregistered}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   145
\newcommand{\isasymordfeminine}{\emph{\rm\textordfeminine}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   146
\newcommand{\isasymordmasculine}{\emph{\rm\textordmasculine}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   147
\newcommand{\isasymsection}{\emph{\S}}
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   148
\newcommand{\isasympounds}{\emph{$\pounds$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   149
\newcommand{\isasymyen}{\emph{\yen}}  %requires amssymb
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   150
\newcommand{\isasymcent}{\emph{\cent}}  %requires wasysym
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   151
\newcommand{\isasymcurrency}{\emph{\currency}}  %requires wasysym
8890
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   152
\newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   153
\newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}}
9a44d8d98731 snapshot of new Isar'ized version;
wenzelm
parents:
diff changeset
   154
\newcommand{\isasymtop}{\emph{$\top$}}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   155
\newcommand{\isasymcong}{\emph{$\cong$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   156
\newcommand{\isasymclubsuit}{\emph{$\clubsuit$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   157
\newcommand{\isasymdiamondsuit}{\emph{$\diamondsuit$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   158
\newcommand{\isasymheartsuit}{\emph{$\heartsuit$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   159
\newcommand{\isasymspadesuit}{\emph{$\spadesuit$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   160
\newcommand{\isasymleftrightarrow}{\emph{$\leftrightarrow$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   161
\newcommand{\isasymge}{\emph{$\ge$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   162
\newcommand{\isasympropto}{\emph{$\propto$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   163
\newcommand{\isasympartial}{\emph{$\partial$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   164
\newcommand{\isasymdots}{\emph{$\dots$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   165
\newcommand{\isasymaleph}{\emph{$\aleph$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   166
\newcommand{\isasymIm}{\emph{$\Im$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   167
\newcommand{\isasymRe}{\emph{$\Re$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   168
\newcommand{\isasymwp}{\emph{$\wp$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   169
\newcommand{\isasymemptyset}{\emph{$\emptyset$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   170
\newcommand{\isasymangle}{\emph{$\angle$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   171
\newcommand{\isasymnabla}{\emph{$\nabla$}}
9767
dc2ee9b2e065 updated;
wenzelm
parents: 9694
diff changeset
   172
\newcommand{\isasymProd}{\emph{$\prod\,$}}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   173
\newcommand{\isasymLeftrightarrow}{\emph{$\Leftrightarrow$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   174
\newcommand{\isasymUparrow}{\emph{$\Uparrow$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   175
\newcommand{\isasymDownarrow}{\emph{$\Downarrow$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   176
\newcommand{\isasymlozenge}{\emph{$\lozenge$}}  %requires amssym
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   177
\newcommand{\isasymlangle}{\emph{$\langle$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   178
\newcommand{\isasymrangle}{\emph{$\rangle$}}
9767
dc2ee9b2e065 updated;
wenzelm
parents: 9694
diff changeset
   179
\newcommand{\isasymSum}{\emph{$\sum\,$}}
dc2ee9b2e065 updated;
wenzelm
parents: 9694
diff changeset
   180
\newcommand{\isasymintegral}{\emph{$\int\,$}}
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   181
\newcommand{\isasymdagger}{\emph{$\dagger$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   182
\newcommand{\isasymsharp}{\emph{$\sharp$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   183
\newcommand{\isasymstar}{\emph{$\star$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   184
\newcommand{\isasymtriangleright}{\emph{$\triangleright$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   185
\newcommand{\isasymlhd}{\emph{$\lhd$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   186
\newcommand{\isasymtriangle}{\emph{$\triangle$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   187
\newcommand{\isasymrhd}{\emph{$\rhd$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   188
\newcommand{\isasymunlhd}{\emph{$\unlhd$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   189
\newcommand{\isasymunrhd}{\emph{$\unrhd$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   190
\newcommand{\isasymtriangleleft}{\emph{$\triangleleft$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   191
\newcommand{\isasymnatural}{\emph{$\natural$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   192
\newcommand{\isasymflat}{\emph{$\flat$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   193
\newcommand{\isasymamalg}{\emph{$\amalg$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   194
\newcommand{\isasymmho}{\emph{$\mho$}}  %requires latexsym
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   195
\newcommand{\isasymupdownarrow}{\emph{$\updownarrow$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   196
\newcommand{\isasymlongmapsto}{\emph{$\longmapsto$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   197
\newcommand{\isasymUpdownarrow}{\emph{$\Updownarrow$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   198
\newcommand{\isasymhookleftarrow}{\emph{$\hookleftarrow$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   199
\newcommand{\isasymhookrightarrow}{\emph{$\hookrightarrow$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   200
\newcommand{\isasymrightleftharpoons}{\emph{$\rightleftharpoons$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   201
\newcommand{\isasymleftharpoondown}{\emph{$\leftharpoondown$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   202
\newcommand{\isasymrightharpoondown}{\emph{$\rightharpoondown$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   203
\newcommand{\isasymleftharpoonup}{\emph{$\leftharpoonup$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   204
\newcommand{\isasymrightharpoonup}{\emph{$\rightharpoonup$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   205
\newcommand{\isasymasymp}{\emph{$\asymp$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   206
\newcommand{\isasymminusplus}{\emph{$\mp$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   207
\newcommand{\isasymbowtie}{\emph{$\bowtie$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   208
\newcommand{\isasymcdots}{\emph{$\cdots$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   209
\newcommand{\isasymodot}{\emph{$\odot$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   210
\newcommand{\isasymsupset}{\emph{$\supset$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   211
\newcommand{\isasymsupseteq}{\emph{$\supseteq$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   212
\newcommand{\isasymsqsupset}{\emph{$\sqsupset$}}  %requires latexsym
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   213
\newcommand{\isasymsqsupseteq}{\emph{$\sqsupseteq$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   214
\newcommand{\isasymll}{\emph{$\ll$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   215
\newcommand{\isasymgg}{\emph{$\gg$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   216
\newcommand{\isasymuplus}{\emph{$\uplus$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   217
\newcommand{\isasymsmile}{\emph{$\smile$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   218
\newcommand{\isasymsucceq}{\emph{$\succeq$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   219
\newcommand{\isasymstileturn}{\emph{$\dashv$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   220
\newcommand{\isasymOr}{\emph{$\bigvee$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   221
\newcommand{\isasymbiguplus}{\emph{$\biguplus$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   222
\newcommand{\isasymddagger}{\emph{$\ddagger$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   223
\newcommand{\isasymJoin}{\emph{$\Join$}}  %requires latexsym
9694
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   224
\newcommand{\isasymbool}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{B}$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   225
\newcommand{\isasymcomplex}{\emph{$\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   226
\newcommand{\isasymnat}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{N}$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   227
\newcommand{\isasymrat}{\emph{$\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   228
\newcommand{\isasymreal}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{R}$}}
13f3aaf12be2 updated;
wenzelm
parents: 8890
diff changeset
   229
\newcommand{\isasymint}{\emph{$\mathsf{Z}\mkern-7.5mu\mathsf{Z}$}}
10005
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   230
\newcommand{\isasymlesssim}{\emph{$\lesssim$}}  %requires amssymb
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   231
\newcommand{\isasymgreatersim}{\emph{$\gtrsim$}}  %requires amssymb
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   232
\newcommand{\isasymlessapprox}{\emph{$\lessapprox$}}  %requires amssymb
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   233
\newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}}  %requires amssymb
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   234
\newcommand{\isasymtriangleq}{\emph{$\triangleq$}}  %requires amssymb
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   235
\newcommand{\isasymlparr}{\emph{$\mathopen{(\mkern-3mu\mid}$}}
8cd7ef5b8f9d updated;
wenzelm
parents: 9845
diff changeset
   236
\newcommand{\isasymrparr}{\emph{$\mathclose{\mid\mkern-3mu)}$}}