etc/symbols
changeset 64556 851ae0e7b09c
parent 63733 7dc86a284456
child 67305 ecb74607063f
     1.1 --- a/etc/symbols	Mon Dec 12 17:40:06 2016 +0100
     1.2 +++ b/etc/symbols	Tue Dec 13 11:51:42 2016 +0100
     1.3 @@ -361,7 +361,7 @@
     1.4  \<comment>              code: 0x002015  group: document  font: IsabelleText
     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 +\<^here>                code: 0x002302  font: IsabelleText
     1.9  \<^undefined>           code: 0x002756  font: IsabelleText
    1.10  \<^noindent>            code: 0x0021e4  group: document  font: IsabelleText
    1.11  \<^smallskip>           code: 0x002508  group: document  font: IsabelleText