|
1826
|
1 |
\documentclass[a4paper,11pt]{article}
|
|
|
2 |
\usepackage{latexsym,amssymb,supertab}
|
|
|
3 |
|
|
|
4 |
\begin{document}
|
|
|
5 |
|
|
|
6 |
\begin{center}
|
|
|
7 |
{\Large
|
|
|
8 |
Description of Isabelle Font \\
|
|
|
9 |
Indexed by Code}\\
|
|
|
10 |
Date: \today
|
|
|
11 |
|
|
|
12 |
\vspace*{.5cm}
|
|
|
13 |
|
|
|
14 |
\tablehead{\hline
|
|
|
15 |
Oct & Dec & Hex & ASCII & \LaTeX & Key Sequence\\
|
|
|
16 |
\hline}
|
|
|
17 |
\tabletail{\hline}
|
|
|
18 |
|
|
|
19 |
\begin{supertabular}{|l|l|l|l|l|l|}
|
|
|
20 |
241 & 161 & a1 & \verb*"\Gamma" & \mbox{$\Gamma$} & Alt G\nextline
|
|
|
21 |
242 & 162 & a2 & \verb*"\Delta" & \mbox{$\Delta$} & Alt D\nextline
|
|
|
22 |
243 & 163 & a3 & \verb*"\Theta" & \mbox{$\Theta$} & Alt J\nextline
|
|
|
23 |
244 & 164 & a4 & \verb*"LAM" & \mbox{$\Lambda$} & Alt L\nextline
|
|
|
24 |
245 & 165 & a5 & \verb*"\Pi" & \mbox{$\Pi$} & Alt P\nextline
|
|
|
25 |
246 & 166 & a6 & \verb*"\Sigma" & \mbox{$\Sigma$} & Alt S\nextline
|
|
|
26 |
247 & 167 & a7 & \verb*"\Phi" & \mbox{$\Phi$} & Alt F\nextline
|
|
|
27 |
250 & 168 & a8 & \verb*"\Psi" & \mbox{$\Psi$} & Alt Q\nextline
|
|
|
28 |
251 & 169 & a9 & \verb*"\Omega" & \mbox{$\Omega$} & Alt W\nextline
|
|
|
29 |
252 & 170 & aa & \verb*"'a" & \mbox{$\alpha$} & Alt a\nextline
|
|
|
30 |
253 & 171 & ab & \verb*"'b" & \mbox{$\beta$} & Alt b\nextline
|
|
|
31 |
254 & 172 & ac & \verb*"'c" & \mbox{$\gamma$} & Alt g\nextline
|
|
|
32 |
255 & 173 & ad & \verb*"\delta" & \mbox{$\delta$} & Alt d\nextline
|
|
|
33 |
256 & 174 & ae & \verb*"\varepsilon" & \mbox{$\varepsilon$} & Alt e\nextline
|
|
|
34 |
257 & 175 & af & \verb*"\zeta" & \mbox{$\zeta$} & Alt z\nextline
|
|
|
35 |
260 & 176 & b0 & \verb*"\eta" & \mbox{$\eta$} & Alt h\nextline
|
|
|
36 |
261 & 177 & b1 & \verb*"\vartheta" & \mbox{$\vartheta$} & Alt j\nextline
|
|
|
37 |
262 & 178 & b2 & \verb*"\kappa" & \mbox{$\kappa$} & Alt k\nextline
|
|
|
38 |
263 & 179 & b3 & \verb*"%" & \mbox{$\lambda$} & Alt l\nextline
|
|
|
39 |
264 & 180 & b4 & \verb*"\mu" & \mbox{$\mu$} & Alt m\nextline
|
|
|
40 |
265 & 181 & b5 & \verb*"\nu" & \mbox{$\nu$} & Alt n\nextline
|
|
|
41 |
266 & 182 & b6 & \verb*"\xi" & \mbox{$\xi$} & Alt x\nextline
|
|
|
42 |
267 & 183 & b7 & \verb*"\pi" & \mbox{$\pi$} & Alt p\nextline
|
|
|
43 |
270 & 184 & b8 & \verb*"'r" & \mbox{$\rho$} & Alt r\nextline
|
|
|
44 |
271 & 185 & b9 & \verb*"'s" & \mbox{$\sigma$} & Alt s\nextline
|
|
|
45 |
272 & 186 & ba & \verb*"'t" & \mbox{$\tau$} & Alt t\nextline
|
|
|
46 |
273 & 187 & bb & \verb*"\varphi" & \mbox{$\varphi$} & Alt f\nextline
|
|
|
47 |
274 & 188 & bc & \verb*"\chi" & \mbox{$\chi$} & Alt c\nextline
|
|
|
48 |
275 & 189 & bd & \verb*"\psi" & \mbox{$\psi$} & Alt q\nextline
|
|
|
49 |
276 & 190 & be & \verb*"\omega" & \mbox{$\omega$} & Alt w\nextline
|
|
|
50 |
277 & 191 & bf & \verb*"~" & \mbox{$\neg$} & AltGraph n\nextline
|
|
|
51 |
300 & 192 & c0 & \verb*"&" & \mbox{$\wedge$} & AltGraph a\nextline
|
|
|
52 |
301 & 193 & c1 & \verb*"|" & \mbox{$\vee$} & AltGraph o\nextline
|
|
|
53 |
302 & 194 & c2 & \verb*"!" & \mbox{$\forall$} & AltGraph f\nextline
|
|
|
54 |
303 & 195 & c3 & \verb*"?" & \mbox{$\exists$} & AltGraph t\nextline
|
|
|
55 |
304 & 196 & c4 & \verb*"!!" & \mbox{$\bigwedge$} & AltGraph F, F9\nextline
|
|
|
56 |
305 & 197 & c5 & \verb*"\lceil" & \mbox{$\lceil$} & Ctrl F5\nextline
|
|
|
57 |
306 & 198 & c6 & \verb*"\rceil" & \mbox{$\rceil$} & Ctrl F6\nextline
|
|
|
58 |
307 & 199 & c7 & \verb*"\lfloor" & \mbox{$\lfloor$} & Ctrl F7\nextline
|
|
|
59 |
310 & 200 & c8 & \verb*"\rfloor" & \mbox{$\rfloor$} & Ctrl F8\nextline
|
|
|
60 |
311 & 201 & c9 & \verb*"(|" & \mbox{$(\!|$} & Ctrl F9\nextline
|
|
|
61 |
312 & 202 & ca & \verb*"|)" & \mbox{$|\!)$} & Ctrl F10\nextline
|
|
|
62 |
313 & 203 & cb & \verb*"[|" & \mbox{$[\![$} & Ctrl F11\nextline
|
|
|
63 |
314 & 204 & cc & \verb*"|]" & \mbox{$]\!]$} & Ctrl F12\nextline
|
|
|
64 |
315 & 205 & cd & \verb*"\emptyset" & \mbox{$\emptyset$} & Alt F10\nextline
|
|
|
65 |
316 & 206 & ce & \verb*":" & \mbox{$\in$} & Alt F11\nextline
|
|
|
66 |
317 & 207 & cf & \verb*"\subseteq" & \mbox{$\subseteq$} & AltGraph F5\nextline
|
|
|
67 |
320 & 208 & d0 & \verb*"Int" & \mbox{$\cap$} & AltGraph F1\nextline
|
|
|
68 |
321 & 209 & d1 & \verb*"Un" & \mbox{$\cup$} & AltGraph F2\nextline
|
|
|
69 |
322 & 210 & d2 & \verb*"Inter" & \mbox{$\bigcap$} & AltGraph F3\nextline
|
|
|
70 |
323 & 211 & d3 & \verb*"Union" & \mbox{$\bigcup$} & AltGraph F4\nextline
|
|
|
71 |
324 & 212 & d4 & \verb*"\sqcap" & \mbox{$\sqcap$} & Ctrl F1\nextline
|
|
|
72 |
325 & 213 & d5 & \verb*"\sqcup" & \mbox{$\sqcup$} & Ctrl F2\nextline
|
|
|
73 |
326 & 214 & d6 & \verb*"glb" & \mbox{$\overline{|\,\,|}$} & Ctrl F3\nextline
|
|
|
74 |
327 & 215 & d7 & \verb*"lub" & \mbox{$\bigsqcup$} & Ctrl F4\nextline
|
|
|
75 |
330 & 216 & d8 & \verb*"UU" & \mbox{$\perp$} & AltGraph b\nextline
|
|
|
76 |
331 & 217 & d9 & \verb*"===" & \mbox{$\doteq$} & AltGraph e\nextline
|
|
|
77 |
332 & 218 & da & \verb*"==" & \mbox{$\equiv$} & AltGraph E, F11\nextline
|
|
|
78 |
333 & 219 & db & \verb*"~=" & \mbox{$\not=$} & AltGraph u, F12\nextline
|
|
|
79 |
334 & 220 & dc & \verb*"\sqsubset" & \mbox{$\sqsubset$} & AltGraph p\nextline
|
|
|
80 |
335 & 221 & dd & \verb*"<<" & \mbox{$\sqsubseteq$} & AltGraph P\nextline
|
|
|
81 |
336 & 222 & de & \verb*"\prec" & \mbox{$\prec$} & AltGraph l\nextline
|
|
|
82 |
337 & 223 & df & \verb*"\preceq" & \mbox{$\preceq$} & AltGraph L\nextline
|
|
|
83 |
340 & 224 & e0 & \verb*"\succ" & \mbox{$\succ$} & AltGraph g\nextline
|
|
|
84 |
341 & 225 & e1 & \verb*"\succeq" & \mbox{$\succeq$} & AltGraph G\nextline
|
|
|
85 |
342 & 226 & e2 & \verb*"\sim" & \mbox{$\sim$} & AltGraph s\nextline
|
|
|
86 |
343 & 227 & e3 & \verb*"\simeq" & \mbox{$\simeq$} & AltGraph S\nextline
|
|
|
87 |
344 & 228 & e4 & \verb*"\le" & \mbox{$\le$} & Shift F11\nextline
|
|
|
88 |
345 & 229 & e5 & \verb*"\ge" & \mbox{$\ge$} & Shift F12\nextline
|
|
|
89 |
346 & 230 & e6 & \verb*"<-" & \mbox{$\leftarrow$} & Alt F1\nextline
|
|
|
90 |
347 & 231 & e7 & \verb*"-" & \mbox{$-$} & Alt F2\nextline
|
|
|
91 |
350 & 232 & e8 & \verb*"->" & \mbox{$\rightarrow$} & Alt F3, AltGraph m\nextline
|
|
|
92 |
351 & 233 & e9 & \verb*"<=" & \mbox{$\Leftarrow$} & Shift F1\nextline
|
|
|
93 |
352 & 234 & ea & \verb*"=" & \mbox{$=$} & Shift F2\nextline
|
|
|
94 |
353 & 235 & eb & \verb*"=>" & \mbox{$\Rightarrow$} & Shift F3, AltGraph M\nextline
|
|
|
95 |
354 & 236 & ec & \verb*"->>" & \mbox{$\twoheadrightarrow$} & Alt F5\nextline
|
|
|
96 |
355 & 237 & ed & \verb*"\mapsto" & \mbox{$\mapsto$} & Alt F6\nextline
|
|
|
97 |
356 & 238 & ee & \verb*"\leadsto" & \mbox{$\leadsto$} & Alt F7\nextline
|
|
|
98 |
357 & 239 & ef & \verb*"\uparrow" & \mbox{$\uparrow$} & Alt F8\nextline
|
|
|
99 |
360 & 240 & f0 & \verb*"\downarrow" & \mbox{$\downarrow$} & Alt F9\nextline
|
|
|
100 |
361 & 241 & f1 & \verb*"~:" & \mbox{$\notin$} & Alt F12\nextline
|
|
|
101 |
362 & 242 & f2 & \verb*"*" & \mbox{$\times$} & AltGraph x\nextline
|
|
|
102 |
363 & 243 & f3 & \verb*"++" & \mbox{$\oplus$} & Shift F5\nextline
|
|
|
103 |
364 & 244 & f4 & \verb*"\ominus" & \mbox{$\ominus$} & Shift F6\nextline
|
|
|
104 |
365 & 245 & f5 & \verb*"**" & \mbox{$\otimes$} & Shift F7\nextline
|
|
|
105 |
366 & 246 & f6 & \verb*"\oslash" & \mbox{$\oslash$} & Shift F8\nextline
|
|
|
106 |
367 & 247 & f7 & \verb*"\natural" & \mbox{$\natural$} & Shift F9, AltGraph N\nextline
|
|
|
107 |
370 & 248 & f8 & \verb*"\infty" & \mbox{$\infty$} & Shift F10\nextline
|
|
|
108 |
371 & 249 & f9 & \verb*"\Box" & \mbox{$\Box$} & AltGraph F6\nextline
|
|
|
109 |
372 & 250 & fa & \verb*"\Diamond" & \mbox{$\Diamond$} & AltGraph F7\nextline
|
|
|
110 |
373 & 251 & fb & \verb*"\circ" & \mbox{$\circ$} & AltGraph F8\nextline
|
|
|
111 |
374 & 252 & fc & \verb*"\bullet" & \mbox{$\bullet$} & AltGraph F9\nextline
|
|
|
112 |
375 & 253 & fd & \verb*"||" & \mbox{$\parallel$} & AltGraph F10\nextline
|
|
|
113 |
376 & 254 & fe & \verb*"\tick" & \mbox{$\surd$} & AltGraph F11\nextline
|
|
|
114 |
377 & 255 & ff & \verb*"\filter" & \mbox{\copyright} & AltGraph F12\\
|
|
|
115 |
\end{supertabular}
|
|
|
116 |
\end{center}
|
|
|
117 |
\end{document}
|