# HG changeset patch
# User wenzelm
# Date 1377855703 -7200
# Node ID dea84641ca353270d1d91bb42ba853cd7eb6c802
# Parent  c3e549e0d3c75a0d8db1fb3d2b370d0710a168f3
more symbol abbrevs, based on ProofGeneral-4.2/isar/isar-unicode-tokens.el and traditional Isabelle/HOL ASCII replacement syntax;

diff -r c3e549e0d3c7 -r dea84641ca35 etc/symbols
--- a/etc/symbols	Fri Aug 30 11:04:29 2013 +0200
+++ b/etc/symbols	Fri Aug 30 11:41:43 2013 +0200
@@ -154,7 +154,7 @@
 \<rat>                  code: 0x00211a  group: letter
 \<real>                 code: 0x00211d  group: letter
 \<int>                  code: 0x002124  group: letter
-\<leftarrow>            code: 0x002190  group: arrow
+\<leftarrow>            code: 0x002190  group: arrow  abbrev: <-
 \<longleftarrow>        code: 0x0027f5  group: arrow
 \<rightarrow>           code: 0x002192  group: arrow  abbrev: ->
 \<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: -->
@@ -162,10 +162,10 @@
 \<Longleftarrow>        code: 0x0027f8  group: arrow
 \<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: =>
 \<Longrightarrow>       code: 0x0027f9  group: arrow  abbrev: ==>
-\<leftrightarrow>       code: 0x002194  group: arrow
-\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <->
-\<Leftrightarrow>       code: 0x0021d4  group: arrow
-\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <=>
+\<leftrightarrow>       code: 0x002194  group: arrow  abbrev: <->
+\<longleftrightarrow>   code: 0x0027f7  group: arrow  abbrev: <->  abbrev: <-->
+\<Leftrightarrow>       code: 0x0021d4  group: arrow  abbrev: <=>
+\<Longleftrightarrow>   code: 0x0027fa  group: arrow  abbrev: <=>  abbrev: <==>
 \<mapsto>               code: 0x0021a6  group: arrow  abbrev: |->
 \<longmapsto>           code: 0x0027fc  group: arrow  abbrev: |-->
 \<midarrow>             code: 0x002500  group: arrow
@@ -175,7 +175,7 @@
 \<leftharpoondown>      code: 0x0021bd  group: arrow
 \<rightharpoondown>     code: 0x0021c1  group: arrow
 \<leftharpoonup>        code: 0x0021bc  group: arrow
-\<rightharpoonup>       code: 0x0021c0  group: arrow
+\<rightharpoonup>       code: 0x0021c0  group: arrow  abbrev: ~=>
 \<rightleftharpoons>    code: 0x0021cc  group: arrow
 \<leadsto>              code: 0x00219d  group: arrow  abbrev: ~>
 \<downharpoonleft>      code: 0x0021c3  group: arrow
@@ -206,12 +206,12 @@
 \<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
 \<bottom>               code: 0x0022a5  group: logic
 \<top>                  code: 0x0022a4  group: logic
-\<and>                  code: 0x002227  group: logic  abbrev: /\
+\<and>                  code: 0x002227  group: logic  abbrev: /\  abbrev: &
 \<And>                  code: 0x0022c0  group: logic  abbrev: !!
-\<or>                   code: 0x002228  group: logic  abbrev: \/
+\<or>                   code: 0x002228  group: logic  abbrev: \/  abbrev: |
 \<Or>                   code: 0x0022c1  group: logic  abbrev: ??
-\<forall>               code: 0x002200  group: logic  abbrev: !
-\<exists>               code: 0x002203  group: logic  abbrev: ?
+\<forall>               code: 0x002200  group: logic  abbrev: !  abbrev: ALL
+\<exists>               code: 0x002203  group: logic  abbrev: ?  abbrev: EX
 \<nexists>              code: 0x002204  group: logic  abbrev: ~?
 \<not>                  code: 0x0000ac  group: logic  abbrev: ~
 \<box>                  code: 0x0025a1  group: logic
@@ -224,8 +224,8 @@
 \<surd>                 code: 0x00221a  group: relation
 \<le>                   code: 0x002264  group: relation  abbrev: <=
 \<ge>                   code: 0x002265  group: relation  abbrev: >=
-\<lless>                code: 0x00226a  group: relation
-\<ggreater>             code: 0x00226b  group: relation
+\<lless>                code: 0x00226a  group: relation  abbrev: <<
+\<ggreater>             code: 0x00226b  group: relation  abbrev: >>
 \<lesssim>              code: 0x002272  group: relation
 \<greatersim>           code: 0x002273  group: relation
 \<lessapprox>           code: 0x002a85  group: relation
@@ -240,21 +240,21 @@
 \<sqsupset>             code: 0x002290  group: relation
 \<sqsubseteq>           code: 0x002291  group: relation  abbrev: [=
 \<sqsupseteq>           code: 0x002292  group: relation  abbrev: =]
-\<inter>                code: 0x002229  group: operator
-\<Inter>                code: 0x0022c2  group: operator
-\<union>                code: 0x00222a  group: operator
-\<Union>                code: 0x0022c3  group: operator
+\<inter>                code: 0x002229  group: operator  abbrev: Int
+\<Inter>                code: 0x0022c2  group: operator  abbrev: Inter
+\<union>                code: 0x00222a  group: operator  abbrev: Un
+\<Union>                code: 0x0022c3  group: operator  abbrev: Union
 \<squnion>              code: 0x002294  group: operator
-\<Squnion>              code: 0x002a06  group: operator
+\<Squnion>              code: 0x002a06  group: operator  abbrev: SUP
 \<sqinter>              code: 0x002293  group: operator
-\<Sqinter>              code: 0x002a05  group: operator
+\<Sqinter>              code: 0x002a05  group: operator  abbrev: INF
 \<setminus>             code: 0x002216  group: operator
 \<propto>               code: 0x00221d  group: operator
 \<uplus>                code: 0x00228e  group: operator
 \<Uplus>                code: 0x002a04  group: operator
 \<noteq>                code: 0x002260  group: relation  abbrev: ~=
 \<sim>                  code: 0x00223c  group: relation
-\<doteq>                code: 0x002250  group: relation
+\<doteq>                code: 0x002250  group: relation  abbrev: =.
 \<simeq>                code: 0x002243  group: relation
 \<approx>               code: 0x002248  group: relation
 \<asymp>                code: 0x00224d  group: relation
@@ -272,12 +272,12 @@
 \<bar>                  code: 0x0000a6  group: punctuation
 \<plusminus>            code: 0x0000b1  group: operator
 \<minusplus>            code: 0x002213  group: operator
-\<times>                code: 0x0000d7  group: operator
+\<times>                code: 0x0000d7  group: operator  abbrev: *
 \<div>                  code: 0x0000f7  group: operator
 \<cdot>                 code: 0x0022c5  group: operator
 \<star>                 code: 0x0022c6  group: operator
 \<bullet>               code: 0x002219  group: operator
-\<circ>                 code: 0x002218  group: operator
+\<circ>                 code: 0x002218  group: operator  abbrev: o
 \<dagger>               code: 0x002020
 \<ddagger>              code: 0x002021
 \<lhd>                  code: 0x0022b2  group: relation