etc/symbols
changeset 55546 76979adf0b96
parent 55044 5f4d5f6876f1
child 55786 96861130f922
     1.1 --- a/etc/symbols	Mon Feb 17 20:54:03 2014 +0100
     1.2 +++ b/etc/symbols	Mon Feb 17 21:37:41 2014 +0100
     1.3 @@ -350,6 +350,7 @@
     1.4  \<newline>              code: 0x0023ce
     1.5  \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
     1.6  \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
     1.7 +\<here>                 code: 0x002302  font: IsabelleText
     1.8  \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
     1.9  \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
    1.10  \<^bold>                code: 0x002759  group: control  font: IsabelleText