etc/symbols
changeset 62260 f82f6c7476a1
parent 62234 7cc9d7b822ae
child 62440 31fa592761da
equal deleted inserted replaced
62259:7afbd7fc32fd 62260:f82f6c7476a1
   355 \<bind>                 code: 0x00291c  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  group: document  font: IsabelleText
   361 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
   361 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
   362 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
   362 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
   363 \<here>                 code: 0x002302  font: IsabelleText
   363 \<here>                 code: 0x002302  font: IsabelleText
   364 \<^undefined>           code: 0x002756  font: IsabelleText
   364 \<^undefined>           code: 0x002756  font: IsabelleText
   365 \<^noindent>            code: 0x0021e4  group: document  font: IsabelleText
   365 \<^noindent>            code: 0x0021e4  group: document  font: IsabelleText