etc/symbols
changeset 69343 395c4fb15ea2
parent 67470 d36fcde7e2c0
child 69361 0d84e3db67c2
equal deleted inserted replaced
69342:fa981730b964 69343:395c4fb15ea2
   356 \<bind>                 code: 0x00291c  abbrev: >>=
   356 \<bind>                 code: 0x00291c  abbrev: >>=
   357 \<then>                 code: 0x002aa2  abbrev: >>
   357 \<then>                 code: 0x002aa2  abbrev: >>
   358 \<some>                 code: 0x0003f5
   358 \<some>                 code: 0x0003f5
   359 \<hole>                 code: 0x002311
   359 \<hole>                 code: 0x002311
   360 \<newline>              code: 0x0023ce
   360 \<newline>              code: 0x0023ce
   361 \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: IsabelleText
   361 \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   362 \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: IsabelleText
   362 \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   363 \<^latex>                               group: document  argument: cartouche
   363 \<^latex>                               group: document  argument: cartouche
   364 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
   364 \<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<
   365 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
   365 \<close>                code: 0x00203a  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: >>
   366 \<^here>                code: 0x002302  font: IsabelleText
   366 \<^here>                code: 0x002302  font: Isabelle␣DejaVu␣Sans␣Mono
   367 \<^undefined>           code: 0x002756  font: IsabelleText
   367 \<^undefined>           code: 0x002756  font: Isabelle␣DejaVu␣Sans␣Mono
   368 \<^noindent>            code: 0x0021e4  group: document  font: IsabelleText
   368 \<^noindent>            code: 0x0021e4  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
   369 \<^smallskip>           code: 0x002508  group: document  font: IsabelleText
   369 \<^smallskip>           code: 0x002508  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
   370 \<^medskip>             code: 0x002509  group: document  font: IsabelleText
   370 \<^medskip>             code: 0x002509  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
   371 \<^bigskip>             code: 0x002501  group: document  font: IsabelleText
   371 \<^bigskip>             code: 0x002501  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
   372 \<^item>                code: 0x0025aa  group: document  font: IsabelleText
   372 \<^item>                code: 0x0025aa  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
   373 \<^enum>                code: 0x0025b8  group: document  font: IsabelleText
   373 \<^enum>                code: 0x0025b8  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
   374 \<^descr>               code: 0x0027a7  group: document  font: IsabelleText
   374 \<^descr>               code: 0x0027a7  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
   375 \<^footnote>            code: 0x00204b  group: document  argument: cartouche  font: IsabelleText
   375 \<^footnote>            code: 0x00204b  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   376 \<^verbatim>            code: 0x0025a9  group: document  argument: cartouche  font: IsabelleText
   376 \<^verbatim>            code: 0x0025a9  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   377 \<^theory_text>         code: 0x002b1a  group: document  argument: cartouche  font: IsabelleText
   377 \<^theory_text>         code: 0x002b1a  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   378 \<^emph>                code: 0x002217  group: document  argument: cartouche  font: IsabelleText
   378 \<^emph>                code: 0x002217  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   379 \<^bold>                code: 0x002759  group: control  argument: cartouche  group: document  font: IsabelleText
   379 \<^bold>                code: 0x002759  group: control  argument: cartouche  group: document  font: Isabelle␣DejaVu␣Sans␣Mono
   380 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
   380 \<^sub>                 code: 0x0021e9  group: control  font: Isabelle␣DejaVu␣Sans␣Mono
   381 \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
   381 \<^sup>                 code: 0x0021e7  group: control  font: Isabelle␣DejaVu␣Sans␣Mono
   382 \<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
   382 \<^bsub>                code: 0x0021d8  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =_(
   383 \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
   383 \<^esub>                code: 0x0021d9  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =_)
   384 \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
   384 \<^bsup>                code: 0x0021d7  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =^(
   385 \<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
   385 \<^esup>                code: 0x0021d6  group: control_block  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: =^)
   386 \<^file>                code: 0x01F5CF  group: icon  argument: cartouche  font: IsabelleText
   386 \<^file>                code: 0x01F5CF  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   387 \<^dir>                 code: 0x01F5C0  group: icon  argument: cartouche  font: IsabelleText
   387 \<^dir>                 code: 0x01F5C0  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   388 \<^url>                 code: 0x01F310  group: icon  argument: cartouche  font: IsabelleText
   388 \<^url>                 code: 0x01F310  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   389 \<^doc>                 code: 0x01F4D3  group: icon  argument: cartouche  font: IsabelleText
   389 \<^doc>                 code: 0x01F4D3  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   390 \<^action>              code: 0x00261b  group: icon  argument: cartouche  font: IsabelleText
   390 \<^action>              code: 0x00261b  group: icon  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
   391 \<^assert>
   391 \<^assert>
   392 \<^binding>             argument: cartouche
   392 \<^binding>             argument: cartouche
   393 \<^class>               argument: cartouche
   393 \<^class>               argument: cartouche
   394 \<^class_syntax>        argument: cartouche
   394 \<^class_syntax>        argument: cartouche
   395 \<^command_keyword>     argument: cartouche
   395 \<^command_keyword>     argument: cartouche