Go back to isabellesym.sty as master symbol list

1 files changed, 441 insertions, 302 deletions

diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index 136e13e6..d8c581a2 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -20,202 +20,182 @@
 
 (defcustom isar-token-name-alist
   '(; token name, unicode char sequence
-   ("alpha" . "α")
-   ("beta" . "β")
-   ("gamma" . "γ")
-   ("delta" . "δ")
-   ("epsilon" . "ϵ")
-   ("varepsilon" . "ε")
-   ("zeta" . "ζ")
-   ("eta" . "η")
-   ("theta" . "θ")
-   ("vartheta" . "ϑ")
-   ("iota" . "ι")
-   ("kappa" . "κ")
-   ("lambda" . "λ")
-   ("mu" . "μ")
-   ("nu" . "ν")
-   ("xi" . "ξ")
-   ("o" . "ø")
-   ("pi" . "π")
-   ("varpi" . "ϖ")
-   ("rho" . "ρ")
-   ("varrho" . "ϱ")
-   ("sigma" . "σ")
-   ("varsigma" . "ς")
-   ("tau" . "τ")
-   ("upsilon" . "υ")
-   ("phi" . "ϕ")
-   ("varphi" . "φ")
-   ("chi" . "χ")
-   ("psi" . "ψ")
-   ("omega" . "ω")
-   ("Gamma" . "Γ")
-   ("Delta" . "Δ")
-   ("Theta" . "Θ")
-   ("Lambda" . "Λ")
-   ("Xi" . "Ξ")
-   ("Pi" . "Π")
-   ("Sigma" . "Σ")
-   ("Upsilon" . "Υ")
-   ("Phi" . "Φ")
-   ("Psi" . "Ψ")
-   ("Omega" . "Ω")
-   ("aleph" . "ℵ")
-   ("hbar" . "ℏ")
-   ("index" . "ı")
-   ("ell" . "ℓ")
-   ("wp" . "℘")
-   ("Re" . "ℜ")
-   ("Im" . "ℑ")
-   ("partial" . "∂")
-   ("infinity" . "∞")
-   ("box" . "□")
-   ("emptyset" . "∅")
-   ("nabla" . "∇")
-   ("surd" . "√")
-   ("top" . "⊤")
-   ("angle" . "∠")
-   ("triangle" . "△")
-   ("Diamond" . "◇")
-   ("exists" . "∃")
-   ("forall" . "∀")
-   ("not" . "¬")
-   ("flat" . "♭")
-   ("natural" . "♮")
-   ("sharp" . "♯")
-   ("clubsuit" . "♣")
-   ("diamondsuit" . "♢")
-   ("heartsuit" . "♡")
-   ("spadesuit" . "♠")
-   ("Sum" . "∑")
-   ("Prod" . "∏")
-   ("Coprod" . "∐")
-   ("integral" . "∫")
-   ("ointegral" . "∮")
-   ("Inter" . "⋂")
-   ("Union" . "⋃")
-   ("Squnion" . "⨆")
-   ("Or" . "⋁")
-   ("And" . "⋀")
-   ("Odot" . "⨀")
-   ("Otimes" . "⨂")
-   ("Oplus" . "⨁")
-   ("Uplus" . "⨄")
-   ("pm" . "±")
-   ("mp" . "∓")
-   ("setminus" . "∖")
-   ("cdot" . "⋅")
-   ("times" . "×")
-   ("ast" . "∗")
-   ("star" . "⋆")
-   ("diamond" . "⋄")
-   ("circ" . "∘")
-   ("bullet" . "∙")
-   ("div" . "÷")
-   ("lhd" . "⊲")
-   ("inter" . "∩")
-   ("union" . "∪")
-   ("uplus" . "⊎")
-   ("sqinter" . "⊓")
-   ("squnion" . "⊔")
-   ("triangleleft" . "◁")
-   ("triangleright" . "▷")
-   ("wr" . "≀")
-   ("bigcirc" . "◯")
-   ("bigtriangleup" . "△")
-   ("bigtriangledown" . "▽")
-   ("rhd" . "⊳")
-   ("or" . "∨")
-   ("and" . "∧")
-   ("oplus" . "⊕")
-   ("ominus" . "⊖")
-   ("otimes" . "⊗")
-   ("oslash" . "⊘")
-   ("odot" . "⊙")
-   ("dagger" . "†")
-   ("ddagger" . "‡")
-   ("amalg" . "⨿")
-   ("unlhd" . "⊴")
-   ("unrhd" . "⊵")
-   ("le" . "≤")
-   ("prec" . "≺")
-   ("preceq" . "≼")
-   ("lless" . "≪")
-   ("subset" . "⊂")
-   ("subseteq" . "⊆")
-   ("sqsubseteq" . "⊑")
-   ("in" . "∈")
-   ("turnstile" . "⊢")
-   ("smile" . "⌣")
-   ("frown" . "⌢")
-   ("sqsubset" . "⊏")
-   ("ge" . "≥")
-   ("succ" . "≻")
-   ("succeq" . "≽")
-   ("ggreater" . "≫")
-   ("supset" . "⊃")
-   ("supseteq" . "⊇")
-   ("sqsupseteq" . "⊒")
-   ("ni" . "∋")
-   ("dashv" . "⊣")
-   ("mid" . "∣")
-   ("parallel" . "∥")
-   ("sqsupset" . "⊐")
-   ("equiv" . "≡")
-   ("sim" . "∼")
-   ("simeq" . "≃")
-   ("asymp" . "≍")
-   ("approx" . "≈")
-   ("cong" . "≅")
-   ("bowtie" . "⋈")
-   ("propto" . "∝")
-   ("Turnstile" . "⊨")
-   ("doteq" . "≐")
-   ("bottom" . "⊥")
-   ("Join" . "⨝")
-   ("nexists" . "∄")
-   ("notlt" . "≮")
-   ("notle" . "≰")
-   ("notprec" . "⊀")
-   ("notpreceq" . "⋠")
-   ("notsubset" . "⊄")
-   ("notsubseteq" . "⊈")
-   ("notsqsubseteq" . "⋢")
-   ("notgt" . "≯")
-   ("notge" . "≱")
-   ("notsucc" . "⊁")
-   ("notsucceq" . "⋡")
-   ("notsupset" . "⊅")
-   ("notsupseteq" . "⊉")
-   ("notsqsupseteq" . "⋣")
-   ("noteq" . "≠")
-   ("notequiv" . "≢")
-   ("notsim" . "≁")
-   ("notsimeq" . "≄")
-   ("notapprox" . "≉")
-   ("notcong" . "≇")
-   ("notasymp" . "≭")
-   ("midarrow" . "–") ; en dash
-   ("leftarrow" . "←")
-   ("Leftarrow" . "⇐")
-   ("rightarrow" . "→")
-   ("Rightarrow" . "⇒")
-   ("leftrightarrow" . "↔")
-   ("Leftrightarrow" . "⇔")
-   ("mapsto" . "↦")
-   ("hookleftarrow" . "↩")
-   ("leftharpoonup" . "↼")
-   ("leftharpoondown" . "↽")
-   ("rightleftharpoons" . "⇌")
-;; Real long symbols, may work in some places
+    ;; Based on isabellesym.sty,v 1.45 2006/01/05
+
+    ;; Bold numerals: here subscripts 
+    ("one" . "₁")
+    ("two" . "₂")
+    ("three" . "₃")
+    ("four" . "₄")
+    ("five" . "₅")
+    ("six" . "₆")
+    ("seven" . "₇")
+    ("eight" . "₈")
+    ("nine" . "₉")
+    ;; Mathcal 
+;;     ("A" . "")
+;;     ("B" . "")
+;;     ("C" . "")
+;;     ("D" . "")
+;;     ("E" . "")
+;;     ("F" . "")
+;;     ("G" . "")
+;;     ("H" . "")
+;;     ("I" . "")
+;;     ("J" . "")
+;;     ("K" . "")
+;;     ("L" . "")
+;;     ("M" . "")
+;;     ("N" . "")
+;;     ("O" . "")
+;;     ("P" . "")
+;;     ("Q" . "")
+;;     ("R" . "")
+;;     ("S" . "")
+;;     ("T" . "")
+;;     ("U" . "")
+;;     ("V" . "")
+;;     ("W" . "")
+;;     ("X" . "")
+;;     ("Y" . "")
+;;     ("Z" . "")
+    ;; Math roman
+;;     ("a" . "")
+;;     ("b" . "")
+;;     ("c" . "")
+;;     ("d" . "")
+;;     ("e" . "")
+;;     ("f" . "")
+;;     ("g" . "")
+;;     ("h" . "")
+;;     ("i" . "")
+;;     ("j" . "")
+;;     ("k" . "")
+;;     ("l" . "")
+;;     ("m" . "")
+;;     ("n" . "")
+;;     ("o" . "")
+;;     ("p" . "")
+;;     ("q" . "")
+;;     ("r" . "")
+;;     ("s" . "")
+;;     ("t" . "")
+;;     ("u" . "")
+;;     ("v" . "")
+;;     ("w" . "")
+;;     ("x" . "")
+;;     ("y" . "")
+;;     ("z" . "")
+    ;; Fraktur
+;;     ("AA" . "")
+;;     ("BB" . "")
+;;     ("CC" . "")
+;;     ("DD" . "")
+;;     ("EE" . "")
+;;     ("FF" . "")
+;;     ("GG" . "")
+;;     ("HH" . "")
+;;     ("II" . "")
+;;     ("JJ" . "")
+;;     ("KK" . "")
+;;     ("LL" . "")
+;;     ("MM" . "")
+;;     ("NN" . "")
+;;     ("OO" . "")
+;;     ("PP" . "")
+;;     ("QQ" . "")
+;;     ("RR" . "")
+;;     ("SS" . "")
+;;     ("TT" . "")
+;;     ("UU" . "")
+;;     ("VV" . "")
+;;     ("WW" . "")
+;;     ("XX" . "")
+;;     ("YY" . "")
+;;     ("ZZ" . "")
+;;     ("aa" . "")
+;;     ("bb" . "")
+;;     ("cc" . "")
+;;     ("dd" . "")
+;;     ("ee" . "")
+;;     ("ff" . "")
+;;     ("gg" . "")
+;;     ("hh" . "")
+;;     ("ii" . "")
+;;     ("jj" . "")
+;;     ("kk" . "")
+;;     ("ll" . "")
+;;     ("mm" . "")
+;;     ("nn" . "")
+;;     ("oo" . "")
+;;     ("pp" . "")
+;;     ("qq" . "")
+;;     ("rr" . "")
+;;     ("ss" . "")
+;;     ("tt" . "")
+;;     ("uu" . "")
+;;     ("vv" . "")
+;;     ("ww" . "")
+;;     ("xx" . "")
+;;     ("yy" . "")
+;;     ("zz" . "")
+    ("alpha" . "α")
+    ("beta" . "β")
+    ("gamma" . "γ")
+    ("delta" . "δ")
+    ("epsilon" . "ε") ; actually varepsilon (some is epsilon)
+    ("zeta" . "ζ")
+    ("eta" . "η")
+    ("theta" . "θ")
+    ("iota" . "ι")
+    ("kappa" . "κ")
+    ("lambda" . "λ")
+    ("mu" . "μ")
+    ("nu" . "ν")
+    ("xi" . "ξ")
+    ("pi" . "π")
+    ("rho" . "ρ")
+    ("sigma" . "σ")
+    ("tau" . "τ")
+    ("upsilon" . "υ")
+    ("phi" . "ϕ")
+    ("chi" . "χ")
+    ("psi" . "ψ")
+    ("omega" . "ω")
+    ("Gamma" . "Γ")
+    ("Delta" . "Δ")
+    ("Theta" . "Θ")
+    ("Lambda" . "Λ")
+    ("Xi" . "Ξ")
+    ("Pi" . "Π")
+    ("Sigma" . "Σ")
+    ("Upsilon" . "Υ")
+    ("Phi" . "Φ")
+    ("Psi" . "Ψ")
+    ("Omega" . "Ω")
+;;  ("bool" . "")
+    ("complex" . "ℂ")
+    ("nat" . "ℕ")
+    ("rat" . "ℚ")
+    ("real" . "ℝ")
+    ("int" . "ℤ")
+    ;; Arrows
+    ("leftarrow" . "←")
+    ("rightarrow" . "→")
+    ("Leftarrow" . "⇐")
+    ("Rightarrow" . "⇒")
+    ("leftrightarrow" . "↔")
+    ("Leftrightarrow" . "⇔")
+    ("mapsto" . "↦")
+    ;; Real long symbols, may work in some places
     ("longleftarrow" . "⟵")
     ("Longleftarrow" . "⟸")
     ("longrightarrow" . "⟶")
     ("Longrightarrow" . "⟹")
     ("longleftrightarrow" . "⟷")
+    ("Longleftrightarrow" . "⟺")
     ("longmapsto" . "⟼")
-;; Faked long symbols, for use otherwise:
+    ;; Faked long symbols, for use otherwise:
 ;;;     ("longleftarrow" . "←–")
 ;;;     ("Longleftarrow" . "⇐–")
 ;;;     ("longrightarrow" . "–→")
@@ -223,118 +203,277 @@
 ;;;     ("longleftrightarrow" . "←→")
 ;;;     ("Longleftrightarrow" . "⇐⇒")
 ;;;     ("longmapsto" . "❘→")
-   ("hookrightarrow" . "↪")
-   ("rightharpoonup" . "⇀")
-   ("rightharpoondown" . "⇁")
-   ("leadsto" . "↝")
-   ("up" . "↑")
-   ("Up" . "⇑")
-   ("down" . "↓")
-   ("Down" . "⇓")
-   ("updown" . "↕")
-   ("Updown" . "⇕")
-   ("nearrow" . "↗")
-   ("searrow" . "↘")
-   ("swarrow" . "↙")
-   ("nwarrow" . "↖")
-   ("lfloor" . "⌊")
-   ("langle" . "⟪")
-   ("lceil" . "⌈")
-   ("langle" . "⟪")
-   ("lbrakk" . "⟦")
-   ("rfloor" . "⌋")
-   ("rangle" . "⟫")
-   ("rceil" . "⌉")
-   ("rangle" . "⟫")
-   ("rbrakk" . "⟧")
-   ("vdots" . "⋮")
-   ("cdots" . "⋯")
-   ("ddots" . "⋱")
-   ("closequote" . "’")
-   ("openquote" . "‘")
-   ("opendblquote" . "”")
-   ("closedblquote" . "“")
-   ("hyphen" . "‐")
-   ("endash" . "–")
-   ("emdash" . "—")
-   ("prime" . "′")
-   ("doubleprime" . "″")
-   ("tripleprime" . "‴")
-   ("quadrupleprime" . "⁗")
-   ("exclamdown" . "¡")
-   ("questiondown" . "¿")
-   ("nbspace" . " ")
-   ("thinspace" . " ")
-   ("copyright" . "©")
-   ("pounds" . "£")
-   ("dots" . "…")
-   ("nat" . "ℕ")
-   ("int" . "ℤ")
-   ("rat" . "ℚ")
-   ("real" . "ℝ")
-   ("complex" . "ℂ")
-   ("notin" . "∉")
-   ("Colon" . "∷")
-   ("bar" . "¦")
-   ("Sqinter" . "⨅")
-   ("guillemotleft" . "«")
-   ("guillemotright" . "»")
-   ("acute" . "´")
-   ("inverse" . "¯¹") ; X-Symb: just "¯"
-   ("notni" . "∌")
-   ("euro" . "€")
-   ("yen" . "¥")
-   ("cent" . "¢")
-   ("mho" . "℧")
-   ("section" . "§")
-   ("paragraph" . "¶")
-   ("registered" . "®")
-   ("degree" . "°")
-   ("onequarter" . "¼")
-   ("onehalf" . "½")
-   ("threequarters" . "¾")
-   ("ordmasculine" . "º")
-   ("ordfeminine" . "ª")
-   ("lparr" . "⦇")
-   ("rparr" . "⦈")
-   ;; these are the subscript numbers, 
-   ;; not bold numerals as in X-Symbol.  
-   ("one" . "₁")
-   ("two" . "₂")
-   ("three" . "₃")
-   ("four" . "₄")
-   ("five" . "₅")
-   ("six" . "₆")
-   ("seven" . "₇")
-   ("eight" . "₈")
-   ("nine" . "₉")
-   ("onesuperior" . "¹")
-   ("twosuperior" . "²")
-   ("threesuperior" . "³")
-   ("foursuperior" . "⁴")
-   ("fivesuperior" . "⁵")
-   ("sixsuperior" . "⁶")
-   ("sevensuperior" . "⁷")
-   ("eightsuperior" . "⁸")
-   ("ninesuperior" . "⁹")
-   ;; not in plain X-Symbol
-   ("oe" . "œ")
-   ("OE" . "Œ")
-   ("ae" . "æ")
-   ("AE" . "Æ")
-   ("aa" . "å")
-   ("AA" . "Å")
-   ("o" . "ø") ;; LaTeX \o
-   ("O" . "Ø") ;; LaTeX \O
-   ("l" . "ł") ;; LaTeX \l
-   ("L" . "Ł") ;; LaTeX \L
-   ("ss" . "ß") ;; LaTeX \ss
-   ("colonequals" . "≔")
-   ("ff" . "ff")
-   ("fi" . "fi")
-   ("fl" . "fl")
-   ("ffi" . "ffi")
-   ("ffl" . "ffl"))
+    ("midarrow" . "–") ; #x002013 en dash
+    ("Midarrow" . "‗") ; #x002017 double low line (not mid)
+    ("hookleftarrow" . "↩")
+    ("hookrightarrow" . "↪")
+    ("leftharpoondown" . "↽")
+    ("rightharpoondown" . "⇁")
+    ("leftharpoonup" . "↼")
+    ("rightharpoonup" . "⇀")
+    ("rightleftharpoons" . "⇌")
+    ("leadsto" . "↝")
+    ("downharpoonleft" . "⇃")
+    ("downharpoonright" . "⇂")
+    ("upharpoonleft" . "↿")
+    ;; ("upharpoonright" . "↾") overlaps restriction
+    ("restriction" . "↾") ;; 
+    ("Colon" . "∷")
+    ("up" . "↑")
+    ("Up" . "⇑")
+    ("down" . "↓")
+    ("Down" . "⇓")
+    ("updown" . "↕")
+    ("Updown" . "⇕")
+    ("langle" . "⟪")
+    ("rangle" . "⟫")
+    ("lceil" . "⌈")
+    ("rceil" . "⌉")
+    ("lfloor" . "⌊")
+    ("rfloor" . "⌋")
+    ("lparr" . "⦇")
+    ("rparr" . "⦈")
+    ("lbrakk" . "⟦")
+    ("rbrakk" . "⟧")
+    ("lbrace" . "")
+    ("rbrace" . "")
+    ("guillemotleft" . "«")
+    ("guillemotright" . "»")
+    ("bottom" . "⊥")
+    ("top" . "⊤")
+    ("and" . "∧")
+    ("And" . "⋀")
+    ("or" . "∨")
+    ("Or" . "⋁")
+    ("forall" . "∀")
+    ("exists" . "∃")
+    ("nexists" . "∄")
+    ("not" . "¬")
+    ("box" . "□")
+    ("diamond" . "◇")
+    ("turnstile" . "⊢")
+    ("Turnstile" . "⊨")
+    ("tturnstile" . "⊩")
+    ("TTurnstile" . "⊫")
+    ("stileturn" . "⊣")
+    ("surd" . "√")
+    ("le" . "≤")
+    ("ge" . "≥")
+    ("lless" . "≪")
+    ("ggreater" . "≫")
+    ("lesssim" . "⪍")
+    ("greatersim" . "⪎")
+    ("lessapprox" . "⪅")
+    ("greaterapprox" . "⪆")
+    ("in" . "∈")
+    ("notin" . "∉")
+    ("subset" . "⊂")
+    ("supset" . "⊃")
+    ("subseteq" . "⊆")
+    ("supseteq" . "⊇")    
+    ("sqsubset" . "⊏")
+    ("sqsupset" . "⊐")
+    ("sqsubseteq" . "⊑")
+    ("sqsupseteq" . "⊒")
+    ("inter" . "∩")
+    ("Inter" . "⋂")
+    ("union" . "∪")
+    ("Union" . "⋃")
+    ("squnion" . "⊔")
+    ("Squnion" . "⨆")
+    ("sqinter" . "⊓")
+    ("Sqinter" . "⨅")
+    ("setminus" . "∖")
+    ("propto" . "∝")
+    ("uplus" . "⊎")
+    ("Uplus" . "⨄")
+    ("noteq" . "≠")
+    ("sim" . "∼")
+    ("doteq" . "≐")
+    ("simeq" . "≃")
+    ("approx" . "≈")
+    ("asymp" . "≍")
+    ("cong" . "≅")
+    ("smile" . "⌣")
+    ("equiv" . "≡")
+    ("frown" . "⌢")
+    ("Join" . "⨝")
+    ("bowtie" . "⋈")
+    ("prec" . "≺")
+    ("succ" . "≻")
+    ("preceq" . "≼")
+    ("succeq" . "≽")
+    ("parallel" . "∥")
+    ("bar" . "¦")
+    ("plusminus" . "±")
+    ("minusplus" . "∓")
+    ("times" . "×")
+    ("div" . "÷")
+    ("cdot" . "⋅")
+    ("star" . "⋆")
+    ("bullet" . "∙")
+    ("circ" . "∘")
+    ("dagger" . "†")
+    ("ddagger" . "‡")
+    ("lhd" . "⊲")
+    ("rhd" . "⊳")
+    ("unlhd" . "⊴")
+    ("unrhd" . "⊵")
+    ("triangleleft" . "◁")
+    ("triangleright" . "▷")
+    ("triangle" . "▵") ; or △
+    ("triangleq" . "≜")
+    ("oplus" . "⊕")
+    ("Oplus" . "⨁")
+    ("otimes" . "⊗")
+    ("Otimes" . "⨂")
+    ("odot" . "⊙")
+    ("Odot" . "⨀")
+    ("ominus" . "⊖")
+    ("oslash" . "⊘") 
+    ("dots" . "…")
+    ("cdots" . "⋯")
+    ("Sum" . "∑")
+    ("Prod" . "∏")
+    ("Coprod" . "∐")
+    ("infinity" . "∞")
+    ("integral" . "∫")
+    ("ointegral" . "∮")
+    ("clubsuit" . "♣")
+    ("diamondsuit" . "♢")
+    ("heartsuit" . "♡")
+    ("spadesuit" . "♠")
+    ("aleph" . "ℵ")
+    ("emptyset" . "∅")
+    ("nabla" . "∇")
+    ("partial" . "∂")
+    ("Re" . "ℜ")
+    ("Im" . "ℑ")
+    ("flat" . "♭")
+    ("natural" . "♮")
+    ("sharp" . "♯")
+    ("angle" . "∠")
+    ("copyright" . "©")
+    ("registered" . "®")
+    ("hyphen" . "‐")
+    ("inverse" . "¯¹") ; X-Symb: just "¯"
+    ("onesuperior" . "¹")
+    ("twosuperior" . "²")
+    ("threesuperior" . "³")
+    ("onequarter" . "¼")
+    ("onehalf" . "½")
+    ("threequarters" . "¾")
+    ("ordmasculine" . "º")
+    ("ordfeminine" . "ª")
+    ("section" . "§")
+    ("paragraph" . "¶")
+    ("exclamdown" . "¡")
+    ("questiondown" . "¿")
+    ("euro" . "€")
+    ("pounds" . "£")
+    ("yen" . "¥")
+    ("cent" . "¢")
+    ("currency" . "¤")
+    ("degree" . "°")
+    ("amalg" . "⨿")
+    ("mho" . "℧")
+    ("lozenge" . "◊")
+    ("wp" . "℘")
+    ("wrong" . "≀") ;; #x002307
+    ("struct" . "")
+    ("acute" . "´")
+    ("index" . "ı")
+    ("dieresis" . "¨")
+    ("cedilla" . "¸")
+    ("hungarumlaut" . "ʺ")
+    ("spacespace" . "⁣⁣") ;; two #x002063
+;    ("module" . "") ??
+    ("some" . "ϵ")
+    
+    ;; Not in Standard Isabelle Symbols
+    ;; (some are in X-Symbols)
+
+    ("stareq" . "≛")
+    ("defeq" . "≝")
+    ("questioneq" . "≟")
+    ("vartheta" . "ϑ")
+    ; ("o" . "ø")
+    ("varpi" . "ϖ")
+    ("varrho" . "ϱ")
+    ("varsigma" . "ς")
+    ("varphi" . "φ")
+    ("hbar" . "ℏ")
+    ("ell" . "ℓ")
+    ("ast" . "∗")
+
+    ("bigcirc" . "◯")
+    ("bigtriangleup" . "△")
+    ("bigtriangledown" . "▽")
+    ("ni" . "∋")
+    ("mid" . "∣")
+    ("notlt" . "≮")
+    ("notle" . "≰")
+    ("notprec" . "⊀")
+    ("notpreceq" . "⋠")
+    ("notsubset" . "⊄")
+    ("notsubseteq" . "⊈")
+    ("notsqsubseteq" . "⋢")
+    ("notgt" . "≯")
+    ("notge" . "≱")
+    ("notsucc" . "⊁")
+    ("notsucceq" . "⋡")
+    ("notsupset" . "⊅")
+    ("notsupseteq" . "⊉")
+    ("notsqsupseteq" . "⋣")
+    ("notequiv" . "≢")
+    ("notsim" . "≁")
+    ("notsimeq" . "≄")
+    ("notapprox" . "≉")
+    ("notcong" . "≇")
+    ("notasymp" . "≭")
+    ("nearrow" . "↗")
+    ("searrow" . "↘")
+    ("swarrow" . "↙")
+    ("nwarrow" . "↖")
+    ("vdots" . "⋮")
+    ("ddots" . "⋱")
+    ("closequote" . "’")
+    ("openquote" . "‘")
+    ("opendblquote" . "”")
+    ("closedblquote" . "“")
+    ("emdash" . "—")
+    ("prime" . "′")
+    ("doubleprime" . "″")
+    ("tripleprime" . "‴")
+    ("quadrupleprime" . "⁗")
+    ("nbspace" . " ")
+    ("thinspace" . " ")
+    ("notni" . "∌")
+    ("colonequals" . "≔")
+
+    ("foursuperior" . "⁴")
+    ("fivesuperior" . "⁵")
+    ("sixsuperior" . "⁶")
+    ("sevensuperior" . "⁷")
+    ("eightsuperior" . "⁸")
+    ("ninesuperior" . "⁹")
+    ;; ligatures, etc, unlikely to be useful?
+    ("oe" . "œ")
+    ("OE" . "Œ")
+    ("ae" . "æ")
+    ("AE" . "Æ")
+    ("aa" . "å")
+    ("AA" . "Å")
+    ("o" . "ø") ;; LaTeX \o
+    ("O" . "Ø") ;; LaTeX \O
+    ("l" . "ł") ;; LaTeX \l
+    ("L" . "Ł") ;; LaTeX \L
+    ("ss" . "ß") ;; LaTeX \ss
+    ("ff" . "ff")
+    ("fi" . "fi")
+    ("fl" . "fl")
+    ("ffi" . "ffi")
+    ("ffl" . "ffl"))
   "Table mapping Isabelle ``xsymbol'' token names to Unicode strings.
 
 You can adjust this table to add more entries, or to change entries for