more symbols;

1 files changed, 89 insertions, 6 deletions

diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el
index 81d20bb6..191eca8c 100644
--- a/isa/x-symbol-isabelle.el
+++ b/isa/x-symbol-isabelle.el
@@ -69,14 +69,14 @@
     (epsilon1 "\\<epsilon>")
     (zeta "\\<zeta>")
     (eta "\\<eta>")
-    (theta1 "\\<theta>")
+    (theta "\\<theta>")
     (kappa1 "\\<kappa>")
     (lambda "\\<lambda>")
     (mu "\\<mu>")
     (nu "\\<nu>")
     (xi "\\<xi>")
     (pi "\\<pi>")
-    (rho "\\<rho>")
+    (rho1 "\\<rho>")
     (sigma "\\<sigma>")
     (tau "\\<tau>")
     (phi1 "\\<phi>")
@@ -126,9 +126,9 @@
     (endash "\\<midarrow>")
     (arrowright "\\<rightarrow>")
     (arrowdblleft "\\<Leftarrow>")
-;   (rightleftharpoons "\\<Midarrow>") ;missing symbol (but not necessary)
+;   (nil "\\<Midarrow>")
     (arrowdblright "\\<Rightarrow>")
-    (frown "\\<bow>")
+    (frown "\\<frown>")
     (mapsto "\\<mapsto>")
     (leadsto "\\<leadsto>")
     (arrowup "\\<up>")
@@ -150,7 +150,11 @@
     (copyright "\\<copyright>")))
 
 (defvar x-symbol-isabelle-xsymbol-table    ; xsymbols
-  '((plusminus "\\<plusminus>")
+  '((Xi "\\<Xi>")
+    (Upsilon1 "\\<Upsilon>")
+    (iota "\\<iota>")
+    (upsilon "\\<upsilon>")
+    (plusminus "\\<plusminus>")
     (division "\\<div>")
     (longarrowright "\\<longrightarrow>")
     (longarrowleft "\\<longleftarrow>")
@@ -183,7 +187,86 @@
     (currency "\\<currency>")
     (braceleft2 "\\<lbrace>")
     (braceright2 "\\<rbrace>")
-    (top "\\<top>")))
+    (top "\\<top>")
+    (congruent "\\<cong>")
+    (club "\\<clubsuit>")
+    (diamond "\\<diamondsuit>")
+    (heart "\\<heartsuit>")
+    (spade "\\<spadesuit>")
+    (arrowboth "\\<leftrightarrow>")
+    (greaterequal "\\<ge>")
+    (proportional "\\<propto>")
+    (partialdiff "\\<partial>")
+    (ellipsis "\\<dots>")
+    (aleph "\\<aleph>")
+    (Ifraktur "\\<Im>")
+    (Rfraktur "\\<Re>")
+    (weierstrass "\\<wp>")
+    (emptyset "\\<emptyset>")
+    (angle "\\<angle>")
+    (gradient "\\<nabla>")
+    (product "\\<Prod>")
+    (arrowdblboth "\\<Leftrightarrow>")
+    (arrowdblup "\\<Uparrow>")
+    (arrowdbldown "\\<Downarrow>")
+    (angleleft "\\<langle>")
+    (angleright "\\<rangle>")
+    (summation "\\<Sum>")
+    (integral "\\<integral>")
+    (dagger "\\<dagger>")
+    (sharp "\\<sharp>")
+    (star "\\<star>")
+    (smltriangleright "\\<triangleright>")
+    (triangleleft "\\<lhd>")
+    (triangle "\\<triangle>")
+    (triangleright "\\<rhd>")
+    (trianglelefteq "\\<unlhd>")
+    (trianglerighteq "\\<unrhd>")
+    (smltriangleleft "\\<triangleleft>")
+    (natural "\\<natural>")
+    (flat "\\<flat>")
+    (amalg "\\<amalg>")
+    (Mho "\\<mho>")
+    (arrowupdown "\\<updownarrow>")
+    (longmapsto "\\<longmapsto>")
+    (arrowdblupdown "\\<Updownarrow>")
+    (hookleftarrow "\\<hookleftarrow>")
+    (hookrightarrow "\\<hookrightarrow>")
+    (rightleftharpoons "\\<rightleftharpoons>")
+    (leftharpoondown "\\<leftharpoondown>")
+    (rightharpoondown "\\<rightharpoondown>")
+    (leftharpoonup "\\<leftharpoonup>")
+    (rightharpoonup "\\<rightharpoonup>")
+    (asym "\\<asymp>")
+    (minusplus "\\<minusplus>")
+    (bowtie "\\<bowtie>")
+    (centraldots "\\<cdots>")
+    (circledot "\\<odot>")
+    (propersuperset "\\<supset>")
+    (reflexsuperset "\\<supseteq>")
+    (propersqsuperset "\\<sqsupset>")
+    (reflexsqsuperset "\\<sqsupseteq>")
+    (lessless "\\<ll>")
+    (greatergreater "\\<gg>")
+    (unionplus "\\<uplus>")
+    (smile "\\<smile>")
+    (reflexsucc "\\<succeq>")
+    (dashbar "\\<stileturn>")
+    (biglogicalor "\\<Or>")
+    (bigunionplus "\\<biguplus>")
+    (daggerdbl "\\<ddagger>")
+    (bigbowtie "\\<Join>")
+    (booleans "\\<bool>")
+    (complexnums "\\<complex>")
+    (natnums "\\<nat>")
+    (rationalnums "\\<rat>")
+    (realnums "\\<real>")
+    (integers "\\<int>")
+    (lesssim "\\<lesssim>")
+    (greatersim "\\<greatersim>")
+    (lessapprox "\\<lessapprox>")
+    (greaterapprox "\\<greaterapprox>")
+    (definedas "\\<triangleq>")))
 
 (defvar x-symbol-isabelle-user-table nil)