7979
|
1 |
%%
|
|
2 |
%% $Id$
|
|
3 |
%%
|
|
4 |
%% definitions of many Isabelle symbols
|
|
5 |
%%
|
|
6 |
|
|
7 |
\usepackage{latexsym}
|
8147
|
8 |
%\usepackage[latin1]{inputenc}
|
7979
|
9 |
|
|
10 |
\newcommand{\bigsqcap}{\overline{|\,\,|}} %just a hack
|
|
11 |
%\def\textbrokenbar??? etc
|
|
12 |
|
|
13 |
\newcommand{\isasymspacespace}{~~}
|
|
14 |
\newcommand{\isasymGamma}{$\Gamma$}
|
|
15 |
\newcommand{\isasymDelta}{$\Delta$}
|
|
16 |
\newcommand{\isasymTheta}{$\Theta$}
|
|
17 |
\newcommand{\isasymLambda}{$\Lambda$}
|
|
18 |
\newcommand{\isasymPi}{$\Pi$}
|
|
19 |
\newcommand{\isasymSigma}{$\Sigma$}
|
|
20 |
\newcommand{\isasymPhi}{$\Phi$}
|
|
21 |
\newcommand{\isasymPsi}{$\Psi$}
|
|
22 |
\newcommand{\isasymOmega}{$\Omega$}
|
|
23 |
\newcommand{\isasymalpha}{$\alpha$}
|
|
24 |
\newcommand{\isasymbeta}{$\beta$}
|
|
25 |
\newcommand{\isasymgamma}{$\gamma$}
|
|
26 |
\newcommand{\isasymdelta}{$\delta$}
|
|
27 |
\newcommand{\isasymepsilon}{$\varepsilon$}
|
|
28 |
\newcommand{\isasymzeta}{$\zeta$}
|
|
29 |
\newcommand{\isasymeta}{$\eta$}
|
|
30 |
\newcommand{\isasymtheta}{$\vartheta$}
|
|
31 |
\newcommand{\isasymkappa}{$\kappa$}
|
|
32 |
\newcommand{\isasymlambda}{$\lambda$}
|
|
33 |
\newcommand{\isasymmu}{$\mu$}
|
|
34 |
\newcommand{\isasymnu}{$\nu$}
|
|
35 |
\newcommand{\isasymxi}{$\xi$}
|
|
36 |
\newcommand{\isasympi}{$\pi$}
|
|
37 |
\newcommand{\isasymrho}{$\rho$}
|
|
38 |
\newcommand{\isasymsigma}{$\sigma$}
|
|
39 |
\newcommand{\isasymtau}{$\tau$}
|
|
40 |
\newcommand{\isasymphi}{$\varphi$}
|
|
41 |
\newcommand{\isasymchi}{$\chi$}
|
|
42 |
\newcommand{\isasympsi}{$\psi$}
|
|
43 |
\newcommand{\isasymomega}{$\omega$}
|
|
44 |
\newcommand{\isasymnot}{\emph{$\neg$}}
|
|
45 |
\newcommand{\isasymand}{\emph{$\wedge$}}
|
|
46 |
\newcommand{\isasymor}{\emph{$\vee$}}
|
8188
|
47 |
\newcommand{\isasymforall}{\emph{$\forall\,$}}
|
|
48 |
\newcommand{\isasymexists}{\emph{$\exists\,$}}
|
|
49 |
\newcommand{\isasymAnd}{\emph{$\bigwedge\,$}}
|
7979
|
50 |
\newcommand{\isasymlceil}{\emph{$\lceil$}}
|
|
51 |
\newcommand{\isasymrceil}{\emph{$\rceil$}}
|
|
52 |
\newcommand{\isasymlfloor}{\emph{$\lfloor$}}
|
|
53 |
\newcommand{\isasymrfloor}{\emph{$\rfloor$}}
|
|
54 |
\newcommand{\isasymturnstile}{\emph{$\vdash$}}
|
|
55 |
\newcommand{\isasymTurnstile}{\emph{$\models$}}
|
|
56 |
\newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}}
|
|
57 |
\newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}}
|
|
58 |
\newcommand{\isasymcdot}{\emph{$\cdot$}}
|
|
59 |
\newcommand{\isasymin}{\emph{$\in$}}
|
|
60 |
\newcommand{\isasymsubseteq}{\emph{$\subseteq$}}
|
|
61 |
\newcommand{\isasyminter}{\emph{$\cap$}}
|
|
62 |
\newcommand{\isasymunion}{\emph{$\cup$}}
|
8188
|
63 |
\newcommand{\isasymInter}{\emph{$\bigcap\,$}}
|
|
64 |
\newcommand{\isasymUnion}{\emph{$\bigcup\,$}}
|
7979
|
65 |
\newcommand{\isasymsqinter}{\emph{$\sqcap$}}
|
|
66 |
\newcommand{\isasymsqunion}{\emph{$\sqcup$}}
|
8188
|
67 |
\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}}
|
|
68 |
\newcommand{\isasymSqunion}{\emph{$\bigsqcup\,$}}
|
7979
|
69 |
\newcommand{\isasymbottom}{\emph{$\bot$}}
|
|
70 |
\newcommand{\isasymdoteq}{\emph{$\doteq$}}
|
|
71 |
\newcommand{\isasymequiv}{\emph{$\equiv$}}
|
|
72 |
\newcommand{\isasymnoteq}{\emph{$\not=$}}
|
|
73 |
\newcommand{\isasymsqsubset}{\emph{$\sqsubset$}}
|
|
74 |
\newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}}
|
|
75 |
\newcommand{\isasymprec}{\emph{$\prec$}}
|
|
76 |
\newcommand{\isasympreceq}{\emph{$\preceq$}}
|
|
77 |
\newcommand{\isasymsucc}{\emph{$\succ$}}
|
|
78 |
\newcommand{\isasymapprox}{\emph{$\approx$}}
|
|
79 |
\newcommand{\isasymsim}{\emph{$\sim$}}
|
|
80 |
\newcommand{\isasymsimeq}{\emph{$\simeq$}}
|
|
81 |
\newcommand{\isasymle}{\emph{$\le$}}
|
|
82 |
\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
|
|
83 |
\newcommand{\isasymleftarrow}{\emph{$\leftarrow$}}
|
|
84 |
\newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated
|
|
85 |
\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}}
|
|
86 |
\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
|
|
87 |
\newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated
|
|
88 |
\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
|
|
89 |
\newcommand{\isasymbow}{\emph{$\frown$}}
|
|
90 |
\newcommand{\isasymmapsto}{\emph{$\mapsto$}}
|
|
91 |
\newcommand{\isasymleadsto}{\emph{$\leadsto$}}
|
|
92 |
\newcommand{\isasymup}{\emph{$\uparrow$}}
|
|
93 |
\newcommand{\isasymdown}{\emph{$\downarrow$}}
|
|
94 |
\newcommand{\isasymnotin}{\emph{$\notin$}}
|
|
95 |
\newcommand{\isasymtimes}{\emph{$\times$}}
|
|
96 |
\newcommand{\isasymoplus}{\emph{$\oplus$}}
|
|
97 |
\newcommand{\isasymominus}{\emph{$\ominus$}}
|
|
98 |
\newcommand{\isasymotimes}{\emph{$\otimes$}}
|
|
99 |
\newcommand{\isasymoslash}{\emph{$\oslash$}}
|
|
100 |
\newcommand{\isasymsubset}{\emph{$\subset$}}
|
|
101 |
\newcommand{\isasyminfinity}{\emph{$\infty$}}
|
|
102 |
\newcommand{\isasymbox}{\emph{$\Box$}}
|
|
103 |
\newcommand{\isasymdiamond}{\emph{$\Diamond$}}
|
|
104 |
\newcommand{\isasymcirc}{\emph{$\circ$}}
|
|
105 |
\newcommand{\isasymbullet}{\emph{$\bullet$}}
|
|
106 |
\newcommand{\isasymparallel}{\emph{$\parallel$}}
|
|
107 |
\newcommand{\isasymsurd}{\emph{$\surd$}}
|
|
108 |
\newcommand{\isasymcopyright}{\emph{\copyright}}
|
|
109 |
|
|
110 |
\newcommand{\isasymplusminus}{\emph{$\pm$}}
|
|
111 |
\newcommand{\isasymdiv}{\emph{$\div$}}
|
|
112 |
\newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}}
|
|
113 |
\newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}}
|
|
114 |
\newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}}
|
|
115 |
\newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}}
|
|
116 |
\newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}}
|
|
117 |
\newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}}
|
|
118 |
%requires OT1 encoding:
|
|
119 |
\newcommand{\isasymbrokenbar}{\emph{\textbrokenbar}}
|
|
120 |
\newcommand{\isasymhyphen}{-}
|
|
121 |
\newcommand{\isasymmacron}{\={}}
|
|
122 |
\newcommand{\isasymexclamdown}{\emph{\textexclamdown}}
|
|
123 |
\newcommand{\isasymquestiondown}{\emph{\textquestiondown}}
|
|
124 |
%requires OT1 encoding:
|
|
125 |
\newcommand{\isasymguillemotleft}{\emph{\guillemotleft}}
|
|
126 |
%requires OT1 encoding:
|
|
127 |
\newcommand{\isasymguillemotright}{\emph{\guillemotright}}
|
|
128 |
%should be available (?):
|
|
129 |
\newcommand{\isasymdegree}{\emph{\textdegree}}
|
|
130 |
\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}}
|
|
131 |
\newcommand{\isasymonequarter}{\emph{\textonequarter}}
|
|
132 |
\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}}
|
|
133 |
\newcommand{\isasymonehalf}{\emph{\textonehalf}}
|
|
134 |
\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}}
|
|
135 |
\newcommand{\isasymthreequarters}{\emph{\textthreequarters}}
|
|
136 |
\newcommand{\isasymparagraph}{\emph{\P}}
|
|
137 |
\newcommand{\isasymregistered}{\emph{\textregistered}}
|
|
138 |
%should be available (?):
|
|
139 |
\newcommand{\isasymordfeminine}{\emph{\textordfeminine}}
|
|
140 |
%should be available (?):
|
|
141 |
\newcommand{\isasymordmasculine}{\emph{\textordmasculine}}
|
|
142 |
\newcommand{\isasymsection}{\S}
|
|
143 |
\newcommand{\isasympounds}{\emph{$\pounds$}}
|
|
144 |
%requires OT1 encoding:
|
|
145 |
\newcommand{\isasymyen}{\emph{\textyen}}
|
|
146 |
%requires OT1 encoding:
|
|
147 |
\newcommand{\isasymcent}{\emph{\textcent}}
|
|
148 |
%requires OT1 encoding:
|
|
149 |
\newcommand{\isasymcurrency}{\emph{\textcurrency}}
|
8680
|
150 |
\newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid\!}$}}
|
8679
|
151 |
\newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}}
|
|
152 |
\newcommand{\isasymtop}{\emph{$\top$}}
|