3 %% |
3 %% |
4 %% definitions of many Isabelle symbols |
4 %% definitions of many Isabelle symbols |
5 %% |
5 %% |
6 |
6 |
7 \usepackage{latexsym} |
7 \usepackage{latexsym} |
|
8 %\usepackage{amssymb} |
8 %\usepackage[latin1]{inputenc} |
9 %\usepackage[latin1]{inputenc} |
9 |
10 |
10 \newcommand{\bigsqcap}{\overline{|\,\,|}} %just a hack |
11 \newcommand{\bigsqcap}{\overline{|\,\,|}} %just a hack |
11 %\def\textbrokenbar??? etc |
12 %\def\textbrokenbar??? etc |
12 |
13 |
13 \newcommand{\isasymspacespace}{~~} |
14 \newcommand{\isasymspacespace}{~~} |
14 \newcommand{\isasymGamma}{$\Gamma$} |
15 \newcommand{\isasymGamma}{$\Gamma$} |
15 \newcommand{\isasymDelta}{$\Delta$} |
16 \newcommand{\isasymDelta}{$\Delta$} |
16 \newcommand{\isasymTheta}{$\Theta$} |
17 \newcommand{\isasymTheta}{$\Theta$} |
17 \newcommand{\isasymLambda}{$\Lambda$} |
18 \newcommand{\isasymLambda}{$\Lambda$} |
|
19 \newcommand{\isasymXi}{$\Xi$} |
18 \newcommand{\isasymPi}{$\Pi$} |
20 \newcommand{\isasymPi}{$\Pi$} |
19 \newcommand{\isasymSigma}{$\Sigma$} |
21 \newcommand{\isasymSigma}{$\Sigma$} |
|
22 \newcommand{\isasymUpsilon}{$\Upsilon$} |
20 \newcommand{\isasymPhi}{$\Phi$} |
23 \newcommand{\isasymPhi}{$\Phi$} |
21 \newcommand{\isasymPsi}{$\Psi$} |
24 \newcommand{\isasymPsi}{$\Psi$} |
22 \newcommand{\isasymOmega}{$\Omega$} |
25 \newcommand{\isasymOmega}{$\Omega$} |
23 \newcommand{\isasymalpha}{$\alpha$} |
26 \newcommand{\isasymalpha}{$\alpha$} |
24 \newcommand{\isasymbeta}{$\beta$} |
27 \newcommand{\isasymbeta}{$\beta$} |
26 \newcommand{\isasymdelta}{$\delta$} |
29 \newcommand{\isasymdelta}{$\delta$} |
27 \newcommand{\isasymepsilon}{$\varepsilon$} |
30 \newcommand{\isasymepsilon}{$\varepsilon$} |
28 \newcommand{\isasymzeta}{$\zeta$} |
31 \newcommand{\isasymzeta}{$\zeta$} |
29 \newcommand{\isasymeta}{$\eta$} |
32 \newcommand{\isasymeta}{$\eta$} |
30 \newcommand{\isasymtheta}{$\vartheta$} |
33 \newcommand{\isasymtheta}{$\vartheta$} |
|
34 \newcommand{\isasymiota}{$\iota$} |
31 \newcommand{\isasymkappa}{$\kappa$} |
35 \newcommand{\isasymkappa}{$\kappa$} |
32 \newcommand{\isasymlambda}{$\lambda$} |
36 \newcommand{\isasymlambda}{$\lambda$} |
33 \newcommand{\isasymmu}{$\mu$} |
37 \newcommand{\isasymmu}{$\mu$} |
34 \newcommand{\isasymnu}{$\nu$} |
38 \newcommand{\isasymnu}{$\nu$} |
35 \newcommand{\isasymxi}{$\xi$} |
39 \newcommand{\isasymxi}{$\xi$} |
36 \newcommand{\isasympi}{$\pi$} |
40 \newcommand{\isasympi}{$\pi$} |
37 \newcommand{\isasymrho}{$\rho$} |
41 \newcommand{\isasymrho}{$\varrho$} |
38 \newcommand{\isasymsigma}{$\sigma$} |
42 \newcommand{\isasymsigma}{$\sigma$} |
39 \newcommand{\isasymtau}{$\tau$} |
43 \newcommand{\isasymtau}{$\tau$} |
|
44 \newcommand{\isasymupsilon}{$\upsilon$} |
40 \newcommand{\isasymphi}{$\varphi$} |
45 \newcommand{\isasymphi}{$\varphi$} |
41 \newcommand{\isasymchi}{$\chi$} |
46 \newcommand{\isasymchi}{$\chi$} |
42 \newcommand{\isasympsi}{$\psi$} |
47 \newcommand{\isasympsi}{$\psi$} |
43 \newcommand{\isasymomega}{$\omega$} |
48 \newcommand{\isasymomega}{$\omega$} |
44 \newcommand{\isasymnot}{\emph{$\neg$}} |
49 \newcommand{\isasymnot}{\emph{$\neg$}} |
84 \newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated |
89 \newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated |
85 \newcommand{\isasymrightarrow}{\emph{$\rightarrow$}} |
90 \newcommand{\isasymrightarrow}{\emph{$\rightarrow$}} |
86 \newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}} |
91 \newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}} |
87 \newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated |
92 \newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated |
88 \newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}} |
93 \newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}} |
89 \newcommand{\isasymbow}{\emph{$\frown$}} |
94 \newcommand{\isasymfrown}{\emph{$\frown$}} |
90 \newcommand{\isasymmapsto}{\emph{$\mapsto$}} |
95 \newcommand{\isasymmapsto}{\emph{$\mapsto$}} |
91 \newcommand{\isasymleadsto}{\emph{$\leadsto$}} |
96 \newcommand{\isasymleadsto}{\emph{$\leadsto$}} |
92 \newcommand{\isasymup}{\emph{$\uparrow$}} |
97 \newcommand{\isasymup}{\emph{$\uparrow$}} |
93 \newcommand{\isasymdown}{\emph{$\downarrow$}} |
98 \newcommand{\isasymdown}{\emph{$\downarrow$}} |
94 \newcommand{\isasymnotin}{\emph{$\notin$}} |
99 \newcommand{\isasymnotin}{\emph{$\notin$}} |
148 %requires OT1 encoding: |
153 %requires OT1 encoding: |
149 \newcommand{\isasymcurrency}{\emph{\textcurrency}} |
154 \newcommand{\isasymcurrency}{\emph{\textcurrency}} |
150 \newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}} |
155 \newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}} |
151 \newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}} |
156 \newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}} |
152 \newcommand{\isasymtop}{\emph{$\top$}} |
157 \newcommand{\isasymtop}{\emph{$\top$}} |
|
158 |
|
159 \newcommand{\isasymcong}{\emph{$\cong$}} |
|
160 \newcommand{\isasymclubsuit}{\emph{$\clubsuit$}} |
|
161 \newcommand{\isasymdiamondsuit}{\emph{$\diamondsuit$}} |
|
162 \newcommand{\isasymheartsuit}{\emph{$\heartsuit$}} |
|
163 \newcommand{\isasymspadesuit}{\emph{$\spadesuit$}} |
|
164 \newcommand{\isasymleftrightarrow}{\emph{$\leftrightarrow$}} |
|
165 \newcommand{\isasymge}{\emph{$\ge$}} |
|
166 \newcommand{\isasympropto}{\emph{$\propto$}} |
|
167 \newcommand{\isasympartial}{\emph{$\partial$}} |
|
168 \newcommand{\isasymdots}{\emph{$\dots$}} |
|
169 \newcommand{\isasymaleph}{\emph{$\aleph$}} |
|
170 \newcommand{\isasymIm}{\emph{$\Im$}} |
|
171 \newcommand{\isasymRe}{\emph{$\Re$}} |
|
172 \newcommand{\isasymwp}{\emph{$\wp$}} |
|
173 \newcommand{\isasymemptyset}{\emph{$\emptyset$}} |
|
174 \newcommand{\isasymangle}{\emph{$\angle$}} |
|
175 \newcommand{\isasymnabla}{\emph{$\nabla$}} |
|
176 \newcommand{\isasymProd}{\emph{$\prod$}} |
|
177 \newcommand{\isasymLeftrightarrow}{\emph{$\Leftrightarrow$}} |
|
178 \newcommand{\isasymUparrow}{\emph{$\Uparrow$}} |
|
179 \newcommand{\isasymDownarrow}{\emph{$\Downarrow$}} |
|
180 \newcommand{\isasymlozenge}{\emph{$\lozenge$}} |
|
181 \newcommand{\isasymlangle}{\emph{$\langle$}} |
|
182 \newcommand{\isasymrangle}{\emph{$\rangle$}} |
|
183 \newcommand{\isasymSum}{\emph{$\sum$}} |
|
184 \newcommand{\isasymintegral}{\emph{$\int$}} |
|
185 \newcommand{\isasymdagger}{\emph{$\dagger$}} |
|
186 \newcommand{\isasymsharp}{\emph{$\sharp$}} |
|
187 \newcommand{\isasymstar}{\emph{$\star$}} |
|
188 \newcommand{\isasymtriangleright}{\emph{$\triangleright$}} |
|
189 \newcommand{\isasymlhd}{\emph{$\lhd$}} |
|
190 \newcommand{\isasymtriangle}{\emph{$\triangle$}} |
|
191 \newcommand{\isasymrhd}{\emph{$\rhd$}} |
|
192 \newcommand{\isasymunlhd}{\emph{$\unlhd$}} |
|
193 \newcommand{\isasymunrhd}{\emph{$\unrhd$}} |
|
194 \newcommand{\isasymtriangleleft}{\emph{$\triangleleft$}} |
|
195 \newcommand{\isasymnatural}{\emph{$\natural$}} |
|
196 \newcommand{\isasymflat}{\emph{$\flat$}} |
|
197 \newcommand{\isasymamalg}{\emph{$\amalg$}} |
|
198 \newcommand{\isasymmho}{\emph{$\mho$}} |
|
199 \newcommand{\isasymupdownarrow}{\emph{$\updownarrow$}} |
|
200 \newcommand{\isasymlongmapsto}{\emph{$\longmapsto$}} |
|
201 \newcommand{\isasymUpdownarrow}{\emph{$\Updownarrow$}} |
|
202 \newcommand{\isasymhookleftarrow}{\emph{$\hookleftarrow$}} |
|
203 \newcommand{\isasymhookrightarrow}{\emph{$\hookrightarrow$}} |
|
204 \newcommand{\isasymrightleftharpoons}{\emph{$\rightleftharpoons$}} |
|
205 \newcommand{\isasymleftharpoondown}{\emph{$\leftharpoondown$}} |
|
206 \newcommand{\isasymrightharpoondown}{\emph{$\rightharpoondown$}} |
|
207 \newcommand{\isasymleftharpoonup}{\emph{$\leftharpoonup$}} |
|
208 \newcommand{\isasymrightharpoonup}{\emph{$\rightharpoonup$}} |
|
209 \newcommand{\isasymasymp}{\emph{$\asymp$}} |
|
210 \newcommand{\isasymminusplus}{\emph{$\mp$}} |
|
211 \newcommand{\isasymbowtie}{\emph{$\bowtie$}} |
|
212 \newcommand{\isasymcdots}{\emph{$\cdots$}} |
|
213 \newcommand{\isasymodot}{\emph{$\odot$}} |
|
214 \newcommand{\isasymsupset}{\emph{$\supset$}} |
|
215 \newcommand{\isasymsupseteq}{\emph{$\supseteq$}} |
|
216 \newcommand{\isasymsqsupset}{\emph{$\sqsupset$}} |
|
217 \newcommand{\isasymsqsupseteq}{\emph{$\sqsupseteq$}} |
|
218 \newcommand{\isasymll}{\emph{$\ll$}} |
|
219 \newcommand{\isasymgg}{\emph{$\gg$}} |
|
220 \newcommand{\isasymuplus}{\emph{$\uplus$}} |
|
221 \newcommand{\isasymsmile}{\emph{$\smile$}} |
|
222 \newcommand{\isasymsucceq}{\emph{$\succeq$}} |
|
223 \newcommand{\isasymstileturn}{\emph{$\dashv$}} |
|
224 \newcommand{\isasymOr}{\emph{$\bigvee$}} |
|
225 \newcommand{\isasymbiguplus}{\emph{$\biguplus$}} |
|
226 \newcommand{\isasymddagger}{\emph{$\ddagger$}} |
|
227 \newcommand{\isasymJoin}{\emph{$\Join$}} |
|
228 \newcommand{\isasymbool}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{B}$}} |
|
229 \newcommand{\isasymcomplex}{\emph{$\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu$}} |
|
230 \newcommand{\isasymnat}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{N}$}} |
|
231 \newcommand{\isasymrat}{\emph{$\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu$}} |
|
232 \newcommand{\isasymreal}{\emph{$\mathrm{I}\mkern-3.8mu\mathrm{R}$}} |
|
233 \newcommand{\isasymint}{\emph{$\mathsf{Z}\mkern-7.5mu\mathsf{Z}$}} |
|
234 |
|
235 %requires amssymb |
|
236 \newcommand{\isasymlesssim}{\emph{$\lesssim$}} |
|
237 \newcommand{\isasymgreatersim}{\emph{$\gtrsim$}} |
|
238 \newcommand{\isasymlessapprox}{\emph{$\lessapprox$}} |
|
239 \newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}} |
|
240 \newcommand{\isasymtriangleq}{\emph{$\triangleq$}} |