update by DvO;

1 files changed, 127 insertions, 128 deletions

diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el
index e724de13..7c0d5ef5 100644
--- a/isa/x-symbol-isa.el
+++ b/isa/x-symbol-isa.el
@@ -45,135 +45,135 @@
 (defvar x-symbol-isa-token-list 'x-symbol-isa-default-token-list)
 
 (defvar x-symbol-isa-symbol-table '(;;symbols (isabelle14 font)
-    (visiblespace () "\\\\<spacespace>")
-    (Gamma () "\\\\<Gamma>")
-    (Delta () "\\\\<Delta>")
-    (Theta () "\\\\<Theta>")
-    (Lambda () "\\\\<Lambda>")
-    (Pi () "\\\\<Pi>")
-    (Sigma () "\\\\<Sigma>")
-    (Phi () "\\\\<Phi>")
-    (Psi () "\\\\<Psi>")
-    (Omega () "\\\\<Omega>")
-    (alpha () "\\\\<alpha>")
-    (beta () "\\\\<beta>")
-    (gamma () "\\\\<gamma>")
-    (delta () "\\\\<delta>")
-    (epsilon1 () "\\\\<epsilon>")
-    (zeta () "\\\\<zeta>")
-    (eta () "\\\\<eta>")
-    (theta1 () "\\\\<theta>")
-    (kappa1 () "\\\\<kappa>")
-    (lambda () "\\\\<lambda>")
-    (mu () "\\\\<mu>")
-    (nu () "\\\\<nu>")
-    (xi () "\\\\<xi>")
-    (pi () "\\\\<pi>")
-    (rho () "\\\\<rho>")
-    (sigma () "\\\\<sigma>")
-    (tau () "\\\\<tau>")
-    (phi1 () "\\\\<phi>")
-    (chi () "\\\\<chi>")
-    (psi () "\\\\<psi>")
-    (omega () "\\\\<omega>")
-    (notsign () "\\\\<not>")
-    (logicaland () "\\\\<and>")
-    (logicalor () "\\\\<or>")
-    (universal1 () "\\\\<forall>")
-    (existential1 () "\\\\<exists>")
-    (biglogicaland () "\\\\<And>")
-    (ceilingleft () "\\\\<lceil>")
-    (ceilingright () "\\\\<rceil>")
-    (floorleft () "\\\\<lfloor>")
-    (floorright () "\\\\<rfloor>")
-    (bardash () "\\\\<turnstile>")
-    (bardashdbl () "\\\\<Turnstile>")
-    (semanticsleft () "\\\\<lbrakk>")
-    (semanticsright () "\\\\<rbrakk>")
-    (periodcentered () "\\\\<cdot>")
-    (element () "\\\\<in>")
-    (reflexsubset () "\\\\<subseteq>")
-    (intersection () "\\\\<inter>")
-    (union () "\\\\<union>")
-    (bigintersection () "\\\\<Inter>")
-    (bigunion () "\\\\<Union>")
-    (sqintersection () "\\\\<sqinter>")
-    (squnion () "\\\\<squnion>")
-    (bigsqintersection () "\\\\<Sqinter>")
-    (bigsqunion () "\\\\<Squnion>")
-    (perpendicular1 () "\\\\<bottom>")
-    (dotequal () "\\\\<doteq>")
-    (equivalence () "\\\\<equiv>")
-    (notequal () "\\\\<noteq>")
-    (propersqsubset () "\\\\<sqsubset>")
-    (reflexsqsubset () "\\\\<sqsubseteq>")
-    (properprec () "\\\\<prec>")
-    (reflexprec () "\\\\<preceq>")
-    (propersucc () "\\\\<succ>")
-    (approxequal () "\\\\<approx>")
-    (similar () "\\\\<sim>")
-    (simequal () "\\\\<simeq>")
-    (lessequal () "\\\\<le>")
-    (coloncolon () "\\\\<Colon>")
-    (arrowleft () "\\\\<leftarrow>")
-    (endash () "\\\\<midarrow>")
-    (arrowright () "\\\\<rightarrow>")
-    (arrowdblleft () "\\\\<Leftarrow>")
-;   (rightleftharpoons () "\\\\<Midarrow>") ;missing symbol (but not necessary)
-    (arrowdblright () "\\\\<Rightarrow>")
-    (frown () "\\\\<bow>")
-    (mapsto () "\\\\<mapsto>")
-    (leadsto () "\\\\<leadsto>")
-    (arrowup () "\\\\<up>")
-    (arrowdown () "\\\\<down>")
-    (notelement () "\\\\<notin>")
-    (multiply () "\\\\<times>")
-    (circleplus () "\\\\<oplus>")
-    (circleminus () "\\\\<ominus>")
-    (circlemultiply () "\\\\<otimes>")
-    (circleslash () "\\\\<oslash>")
-    (propersubset () "\\\\<subset>")
-    (infinity () "\\\\<infinity>")
-    (box () "\\\\<box>")
-    (lozenge1 () "\\\\<diamond>")
-    (circ () "\\\\<circ>")
-    (bullet () "\\\\<bullet>")
-    (bardbl () "\\\\<parallel>")
-    (radical () "\\\\<surd>")
-    (copyright () "\\\\<copyright>")
+    (visiblespace () "\\\\<spacespace>" "\\<spacespace>")
+    (Gamma  () "\\\\<Gamma>" "\\<Gamma>")
+    (Delta  () "\\\\<Delta>" "\\<Delta>")
+    (Theta  () "\\\\<Theta>" "\\<Theta>")
+    (Lambda () "\\\\<Lambda>" "\\<Lambda>")
+    (Pi     () "\\\\<Pi>" "\\<Pi>")
+    (Sigma  () "\\\\<Sigma>" "\\<Sigma>")
+    (Phi    () "\\\\<Phi>" "\\<Phi>")
+    (Psi    () "\\\\<Psi>" "\\<Psi>")
+    (Omega  () "\\\\<Omega>" "\\<Omega>")
+    (alpha  () "\\\\<alpha>" "\\<alpha>")
+    (beta   () "\\\\<beta>" "\\<beta>")
+    (gamma  () "\\\\<gamma>" "\\<gamma>")
+    (delta  () "\\\\<delta>" "\\<delta>")
+    (epsilon1 () "\\\\<epsilon>" "\\<epsilon>")
+    (zeta   () "\\\\<zeta>" "\\<zeta>")
+    (eta    () "\\\\<eta>" "\\<eta>")
+    (theta1 () "\\\\<theta>" "\\<theta>")
+    (kappa1 () "\\\\<kappa>" "\\<kappa>")
+    (lambda () "\\\\<lambda>" "\\<lambda>")
+    (mu     () "\\\\<mu>" "\\<mu>")
+    (nu     () "\\\\<nu>" "\\<nu>")
+    (xi     () "\\\\<xi>" "\\<xi>")
+    (pi     () "\\\\<pi>" "\\<pi>")
+    (rho    () "\\\\<rho>" "\\<rho>")
+    (sigma  () "\\\\<sigma>" "\\<sigma>")
+    (tau    () "\\\\<tau>" "\\<tau>")
+    (phi1   () "\\\\<phi>" "\\<phi>")
+    (chi    () "\\\\<chi>" "\\<chi>")
+    (psi    () "\\\\<psi>" "\\<psi>")
+    (omega  () "\\\\<omega>" "\\<omega>")
+    (notsign       () "\\\\<not>" "\\<not>")
+    (logicaland    () "\\\\<and>" "\\<and>")
+    (logicalor     () "\\\\<or>" "\\<or>")
+    (universal1    () "\\\\<forall>" "\\<forall>")
+    (existential1  () "\\\\<exists>" "\\<exists>")
+    (biglogicaland () "\\\\<And>" "\\<And>")
+    (ceilingleft   () "\\\\<lceil>" "\\<lceil>")
+    (ceilingright  () "\\\\<rceil>" "\\<rceil>")
+    (floorleft     () "\\\\<lfloor>" "\\<lfloor>")
+    (floorright    () "\\\\<rfloor>" "\\<rfloor>")
+    (bardash       () "\\\\<turnstile>" "\\<turnstile>")
+    (bardashdbl    () "\\\\<Turnstile>" "\\<Turnstile>")
+    (semanticsleft () "\\\\<lbrakk>" "\\<lbrakk>")
+    (semanticsright () "\\\\<rbrakk>" "\\<rbrakk>")
+    (periodcentered () "\\\\<cdot>" "\\<cdot>")
+    (element      () "\\\\<in>" "\\<in>")
+    (reflexsubset () "\\\\<subseteq>" "\\<subseteq>")
+    (intersection () "\\\\<inter>" "\\<inter>")
+    (union        () "\\\\<union>" "\\<union>")
+    (bigintersection   () "\\\\<Inter>" "\\<Inter>")
+    (bigunion          () "\\\\<Union>" "\\<Union>")
+    (sqintersection    () "\\\\<sqinter>" "\\<sqinter>")
+    (squnion           () "\\\\<squnion>" "\\<squnion>")
+    (bigsqintersection () "\\\\<Sqinter>" "\\<Sqinter>")
+    (bigsqunion        () "\\\\<Squnion>" "\\<Squnion>")
+    (perpendicular1    () "\\\\<bottom>" "\\<bottom>")
+    (dotequal    () "\\\\<doteq>" "\\<doteq>")
+    (equivalence () "\\\\<equiv>" "\\<equiv>")
+    (notequal    () "\\\\<noteq>" "\\<noteq>")
+    (propersqsubset () "\\\\<sqsubset>" "\\<sqsubset>")
+    (reflexsqsubset () "\\\\<sqsubseteq>" "\\<sqsubseteq>")
+    (properprec  () "\\\\<prec>" "\\<prec>")
+    (reflexprec  () "\\\\<preceq>" "\\<preceq>")
+    (propersucc  () "\\\\<succ>" "\\<succ>")
+    (approxequal () "\\\\<approx>" "\\<approx>")
+    (similar     () "\\\\<sim>" "\\<sim>")
+    (simequal    () "\\\\<simeq>" "\\<simeq>")
+    (lessequal   () "\\\\<le>" "\\<le>")
+    (coloncolon  () "\\\\<Colon>" "\\<Colon>")
+    (arrowleft   () "\\\\<leftarrow>" "\\<leftarrow>")
+    (endash      () "\\\\<midarrow>" "\\<midarrow>")
+    (arrowright  () "\\\\<rightarrow>" "\\<rightarrow>")
+    (arrowdblleft () "\\\\<Leftarrow>" "\\<Leftarrow>")
+;   (rightleftharpoons () "\\\\<Midarrow>" "\\<Midarrow>") ;missing symbol (but not necessary)
+    (arrowdblright () "\\\\<Rightarrow>" "\\<Rightarrow>")
+    (frown () "\\\\<bow>" "\\<bow>")
+    (mapsto () "\\\\<mapsto>" "\\<mapsto>")
+    (leadsto () "\\\\<leadsto>" "\\<leadsto>")
+    (arrowup () "\\\\<up>" "\\<up>")
+    (arrowdown () "\\\\<down>" "\\<down>")
+    (notelement () "\\\\<notin>" "\\<notin>")
+    (multiply () "\\\\<times>" "\\<times>")
+    (circleplus () "\\\\<oplus>" "\\<oplus>")
+    (circleminus () "\\\\<ominus>" "\\<ominus>")
+    (circlemultiply () "\\\\<otimes>" "\\<otimes>")
+    (circleslash () "\\\\<oslash>" "\\<oslash>")
+    (propersubset () "\\\\<subset>" "\\<subset>")
+    (infinity () "\\\\<infinity>" "\\<infinity>")
+    (box () "\\\\<box>" "\\<box>")
+    (lozenge1 () "\\\\<diamond>" "\\<diamond>")
+    (circ () "\\\\<circ>" "\\<circ>")
+    (bullet () "\\\\<bullet>" "\\<bullet>")
+    (bardbl () "\\\\<parallel>" "\\<parallel>")
+    (radical () "\\\\<surd>" "\\<surd>")
+    (copyright () "\\\\<copyright>" "\\<copyright>")
   ))
 (defvar x-symbol-isa-xsymbol-table '(;;xsymbols
-    (plusminus () "\\\\<plusminus>")
-    (division () "\\\\<div>")
-    (longarrowright () "\\\\<longrightarrow>")
-    (longarrowleft  () "\\\\<longleftarrow>")
-    (longarrowboth  () "\\\\<longleftrightarrow>")
-    (longarrowdblright () "\\\\<Longrightarrow>")
-    (longarrowdblleft  () "\\\\<Longleftarrow>")
-    (longarrowdblboth  () "\\\\<Longleftrightarrow>")
-    (brokenbar () "\\\\<brokenbar>")
-    (hyphen () "\\\\<hyphen>")
-    (macron () "\\\\<macron>")
-    (exclamdown () "\\\\<exclamdown>")
-    (questiondown () "\\\\<questiondown>")
-    (guillemotleft () "\\\\<guillemotleft>")
-    (guillemotright () "\\\\<guillemotright>")
-    (degree () "\\\\<degree>")
-    (onesuperior () "\\\\<onesuperior>")
-    (onequarter () "\\\\<onequarter>")
-    (twosuperior () "\\\\<twosuperior>")
-    (onehalf () "\\\\<onehalf>")
-    (threesuperior () "\\\\<threesuperior>")
-    (threequarters () "\\\\<threequarters>")
-    (paragraph () "\\\\<paragraph>")
-    (registered () "\\\\<registered>")
-    (ordfeminine () "\\\\<ordfeminine>")
-    (ordmasculine () "\\\\<ordmasculine>")
-    (section () "\\\\<section>")
-    (pounds () "\\\\<pounds>")
-    (yen () "\\\\<yen>")
-    (cent () "\\\\<cent>")
-    (currency () "\\\\<currency>")
+    (plusminus () "\\\\<plusminus>" "\\<plusminus>")
+    (division () "\\\\<div>" "\\<div>")
+    (longarrowright () "\\\\<longrightarrow>" "\\<longrightarrow>")
+    (longarrowleft  () "\\\\<longleftarrow>" "\\<longleftarrow>")
+    (longarrowboth  () "\\\\<longleftrightarrow>" "\\<longleftrightarrow>")
+    (longarrowdblright () "\\\\<Longrightarrow>" "\\<Longrightarrow>")
+    (longarrowdblleft  () "\\\\<Longleftarrow>" "\\<Longleftarrow>")
+    (longarrowdblboth  () "\\\\<Longleftrightarrow>" "\\<Longleftrightarrow>")
+    (brokenbar () "\\\\<brokenbar>" "\\<brokenbar>")
+    (hyphen () "\\\\<hyphen>" "\\<hyphen>")
+    (macron () "\\\\<macron>" "\\<macron>")
+    (exclamdown () "\\\\<exclamdown>" "\\<exclamdown>")
+    (questiondown () "\\\\<questiondown>" "\\<questiondown>")
+    (guillemotleft () "\\\\<guillemotleft>" "\\<guillemotleft>")
+    (guillemotright () "\\\\<guillemotright>" "\\<guillemotright>")
+    (degree () "\\\\<degree>" "\\<degree>")
+    (onesuperior () "\\\\<onesuperior>" "\\<onesuperior>")
+    (onequarter () "\\\\<onequarter>" "\\<onequarter>")
+    (twosuperior () "\\\\<twosuperior>" "\\<twosuperior>")
+    (onehalf () "\\\\<onehalf>" "\\<onehalf>")
+    (threesuperior () "\\\\<threesuperior>" "\\<threesuperior>")
+    (threequarters () "\\\\<threequarters>" "\\<threequarters>")
+    (paragraph () "\\\\<paragraph>" "\\<paragraph>")
+    (registered () "\\\\<registered>" "\\<registered>")
+    (ordfeminine () "\\\\<ordfeminine>" "\\<ordfeminine>")
+    (ordmasculine () "\\\\<ordmasculine>" "\\<ordmasculine>")
+    (section () "\\\\<section>" "\\<section>")
+    (pounds () "\\\\<pounds>" "\\<pounds>")
+    (yen () "\\\\<yen>" "\\<yen>")
+    (cent () "\\\\<cent>" "\\<cent>")
+    (currency () "\\\\<currency>" "\\<currency>")
   ))
 (defvar x-symbol-isa-user-table nil)
 (defvar x-symbol-isa-table
@@ -219,6 +219,5 @@
 (global-set-key [(meta e)] 'x-symbol-INSERT-equivalence)
 (global-set-key [(meta u)] 'x-symbol-INSERT-notequal)
 (global-set-key [(meta m)] 'x-symbol-INSERT-arrowdblright)
-(global-set-key [(meta x)] 'x-symbol-INSERT-multiply)
 
 (global-set-key [(meta i)] 'x-symbol-INSERT-longarrowright)