# HG changeset patch
# User wenzelm
# Date 1377858255 -7200
# Node ID 17b887110cc14b870e56c4e1f17e2a787657a377
# Parent  5f310fb79c62462b8f685297ef4e1e433f7a411e
more symbol abbrevs;

diff -r 5f310fb79c62 -r 17b887110cc1 etc/symbols
--- a/etc/symbols	Fri Aug 30 12:10:34 2013 +0200
+++ b/etc/symbols	Fri Aug 30 12:24:15 2013 +0200
@@ -192,10 +192,10 @@
 \<Updown>               code: 0x0021d5  group: arrow
 \<langle>               code: 0x0027e8  group: punctuation  abbrev: <<
 \<rangle>               code: 0x0027e9  group: punctuation  abbrev: >>
-\<lceil>                code: 0x002308  group: punctuation
-\<rceil>                code: 0x002309  group: punctuation
-\<lfloor>               code: 0x00230a  group: punctuation
-\<rfloor>               code: 0x00230b  group: punctuation
+\<lceil>                code: 0x002308  group: punctuation  abbrev: [.
+\<rceil>                code: 0x002309  group: punctuation  abbrev: .]
+\<lfloor>               code: 0x00230a  group: punctuation  abbrev: [.
+\<rfloor>               code: 0x00230b  group: punctuation  abbrev: .]
 \<lparr>                code: 0x002987  group: punctuation  abbrev: (|
 \<rparr>                code: 0x002988  group: punctuation  abbrev: |)
 \<lbrakk>               code: 0x0027e6  group: punctuation  abbrev: [|
@@ -269,7 +269,7 @@
 \<preceq>               code: 0x00227c  group: relation
 \<succeq>               code: 0x00227d  group: relation
 \<parallel>             code: 0x002225  group: punctuation  abbrev: ||
-\<bar>                  code: 0x0000a6  group: punctuation
+\<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
 \<plusminus>            code: 0x0000b1  group: operator
 \<minusplus>            code: 0x002213  group: operator
 \<times>                code: 0x0000d7  group: operator  abbrev: *