From 2a23ee3322e4274c110278a447a95133ea428b79 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 4 Feb 2008 12:39:22 +0000 Subject: Go back to isabellesym.sty as master symbol list --- isar/isar-unicode-tokens.el | 743 ++++++++++++++++++++++++++------------------ 1 file changed, 441 insertions(+), 302 deletions(-) (limited to 'isar/isar-unicode-tokens.el') 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 -- cgit v1.2.3