Description of Isabelle Font Indexed by Code

Date: June 25, 1996

Oct Dec Hex ASCII  L^{A}TEX Key Sequence
241 161 a1 \Gamma       Γ  Alt G
242 162 a2 \Delta       Δ  Alt D
243 163 a3 \Theta       Θ  Alt J
244 164 a4 LAM          Λ  Alt L
245 165 a5 \Pi          Π  Alt P
246 166 a6 \Sigma       Σ  Alt S
247 167 a7 \Phi         Φ  Alt F
250 168 a8 \Psi         Ψ  Alt Q
251 169 a9 \Omega       Ω  Alt W
252 170 aa 'a           α  Alt a
253 171 ab 'b           β  Alt b
254 172 ac 'c           γ  Alt g
255 173 ad \delta       δ  Alt d
256 174 ae \varepsilon  ε  Alt e
257 175 af  \zeta        ζ  Alt z
260 176 b0 \eta         η  Alt h
261 177 b1 \vartheta    ϑ  Alt j
262 178 b2 \kappa       κ  Alt k
263 179 b3 %            λ  Alt l
264 180 b4 \mu          μ  Alt m
265 181 b5 \nu          ν  Alt n
266 182 b6 \xi          ξ  Alt x
267 183 b7 \pi          π  Alt p
270 184 b8 'r           ρ  Alt r
271 185 b9 's           σ  Alt s
272 186 ba 't           τ  Alt t
273 187 bb \varphi      φ  Alt f
274 188 bc \chi         χ  Alt c
275 189 bd \psi         ψ  Alt q
276 190 be \omega       ω  Alt w
277 191 bf ~            ¬  AltGraph n
300 192 c0 &            ∧  AltGraph a
301 193 c1 |            ∨  AltGraph o
302 194 c2 !            ∀  AltGraph f
303 195 c3 ?            ∃  AltGraph t
304 196 c4 !!           ⋀  AltGraph F, F9
305 197 c5 \lceil       ⌈  Ctrl F5
306 198 c6 \rceil       ⌉  Ctrl F6

Oct Dec Hex ASCII  L^{A}TEX Key Sequence
307 199 c7 \lfloor    ⌊  Ctrl F7
310 200 c8 \rfloor    ⌋  Ctrl F8
311 201 c9 (|         (|  Ctrl F9
312 202 ca |)         |)  Ctrl F10
313 203 cb [|         [[  Ctrl F11
314 204 cc |]         ]]  Ctrl F12
315 205 cd \emptyset  ∅  Alt F10
316 206 ce :          ∈  Alt F11
317 207 cf  \subseteq  ⊆  AltGraph F5
320 208 d0 Int        ∩  AltGraph F1
321 209 d1 Un         ∪  AltGraph F2
322 210 d2 Inter      ⋂  AltGraph F3
323 211 d3 Union      ⋃  AltGraph F4
324 212 d4 \sqcap     ⊓  Ctrl F1
325 213 d5 \sqcup     ⊔  Ctrl F2
326 214 d6 glb        \overline{| |}  Ctrl F3
327 215 d7 lub        ⨆  Ctrl F4
330 216 d8 UU         ⊥  AltGraph b
331 217 d9 ===        ≐  AltGraph e
332 218 da ==         ≡  AltGraph E, F11
333 219 db ~=         ≠  AltGraph u, F12
334 220 dc \sqsubset  ⊏  AltGraph p
335 221 dd <<         ⊑  AltGraph P
336 222 de \prec      ≺  AltGraph l
337 223 df \preceq    ⪯  AltGraph L
340 224 e0 \succ      ≻  AltGraph g
341 225 e1 \succeq    ⪰  AltGraph G
342 226 e2 \sim       ∼  AltGraph s
343 227 e3 \simeq     ≃  AltGraph S
344 228 e4 \le        ≤  Shift F11
345 229 e5 \ge        ≥  Shift F12
346 230 e6 <-         ←  Alt F1
347 231 e7 -          −  Alt F2
350 232 e8 ->         →  Alt F3, AltGraph m
351 233 e9 <=         ⇐  Shift F1
352 234 ea =          =  Shift F2
353 235 eb =>         ⇒  Shift F3, AltGraph M
354 236 ec ->>        ↠  Alt F5

Oct Dec Hex ASCII  L^{A}TEX Key Sequence
355 237 ed \mapsto     ↦  Alt F6
356 238 ee \leadsto    ⇝  Alt F7
357 239 ef  \uparrow    ↑  Alt F8
360 240 f0  \downarrow  ↓  Alt F9
361 241 f1  ~:          ∉  Alt F12
362 242 f2  *           ×  AltGraph x
363 243 f3  ++          ⊕  Shift F5
364 244 f4  \ominus     ⊖  Shift F6
365 245 f5  **          ⊗  Shift F7
366 246 f6  \oslash     ⊘  Shift F8
367 247 f7  \natural    ♮  Shift F9, AltGraph N
370 248 f8  \infty      ∞  Shift F10
371 249 f9  \Box        □  AltGraph F6
372 250 fa  \Diamond    ◇  AltGraph F7
373 251 fb \circ       ∘  AltGraph F8
374 252 fc  \bullet     •  AltGraph F9
375 253 fd ||          ∥  AltGraph F10
376 254 fe  \tick       √  AltGraph F11
377 255 ff  \filter     \begin{matrix}c \\ ◯ \end{matrix}  AltGraph F12