diff -r 0e5fa27d3293 -r 5fc1c2098964 etc/symbols --- a/etc/symbols Sat May 24 12:55:09 2014 +0200 +++ b/etc/symbols Sat May 24 12:58:22 2014 +0200 @@ -348,8 +348,8 @@ \ code: 0x0002dd \ code: 0x0003f5 \ code: 0x0023ce -\ code: 0x002039 group: punctuation font: IsabelleText -\ code: 0x00203a group: punctuation font: IsabelleText +\ code: 0x002039 group: punctuation font: IsabelleText abbrev: << +\ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \ code: 0x002302 font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText