etc/symbols
changeset 55033 8e8243975860
parent 55015 e33c5bd729ff
child 55044 5f4d5f6876f1
     1.1 --- a/etc/symbols	Fri Jan 17 20:51:36 2014 +0100
     1.2 +++ b/etc/symbols	Sat Jan 18 19:15:12 2014 +0100
     1.3 @@ -348,6 +348,8 @@
     1.4  \<hungarumlaut>         code: 0x0002dd
     1.5  \<some>                 code: 0x0003f5
     1.6  \<newline>              code: 0x0023ce
     1.7 +\<open>                 code: 0x002039  abbrev: <<  font: IsabelleText
     1.8 +\<close>                code: 0x00203a  abbrev: >>  font: IsabelleText
     1.9  \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
    1.10  \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
    1.11  \<^bold>                code: 0x002759  group: control  font: IsabelleText