etc/symbols
changeset 62025 8007e4ff493a
parent 62023 19605292757e
child 62108 0046bacc5f5b
equal deleted inserted replaced
62024:e3e22a5e85f2 62025:8007e4ff493a
   350 \<acute>                code: 0x0000b4
   350 \<acute>                code: 0x0000b4
   351 \<index>                code: 0x000131
   351 \<index>                code: 0x000131
   352 \<dieresis>             code: 0x0000a8
   352 \<dieresis>             code: 0x0000a8
   353 \<cedilla>              code: 0x0000b8
   353 \<cedilla>              code: 0x0000b8
   354 \<hungarumlaut>         code: 0x0002dd
   354 \<hungarumlaut>         code: 0x0002dd
   355 \<bind>                 code: 0x00291c  abbrev: >>  abbrev: >>=
   355 \<bind>                 code: 0x00291c  abbrev: >>=
   356 \<then>                 code: 0x002aa2  abbrev: >>
   356 \<then>                 code: 0x002aa2  abbrev: >>
   357 \<some>                 code: 0x0003f5
   357 \<some>                 code: 0x0003f5
   358 \<hole>                 code: 0x002311
   358 \<hole>                 code: 0x002311
   359 \<newline>              code: 0x0023ce
   359 \<newline>              code: 0x0023ce
   360 \<comment>              code: 0x002015  font: IsabelleText
   360 \<comment>              code: 0x002015  font: IsabelleText