350 \<hole> code: 0x002311 |
350 \<hole> code: 0x002311 |
351 \<newline> code: 0x0023ce |
351 \<newline> code: 0x0023ce |
352 \<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: << |
352 \<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: << |
353 \<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >> |
353 \<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >> |
354 \<here> code: 0x002302 font: IsabelleText |
354 \<here> code: 0x002302 font: IsabelleText |
|
355 \<^noindent> code: 0x0021e4 group: control font: IsabelleText |
|
356 \<^smallskip> code: 0x002508 group: control font: IsabelleText |
|
357 \<^medskip> code: 0x002509 group: control font: IsabelleText |
|
358 \<^bigskip> code: 0x002501 group: control font: IsabelleText |
|
359 \<^item> code: 0x0025aa group: control font: IsabelleText |
|
360 \<^enum> code: 0x0025b8 group: control font: IsabelleText |
|
361 \<^descr> code: 0x0027a7 group: control font: IsabelleText |
|
362 \<^emph> code: 0x002217 group: control font: IsabelleText |
|
363 \<^bold> code: 0x002759 group: control font: IsabelleText |
355 \<^sub> code: 0x0021e9 group: control font: IsabelleText |
364 \<^sub> code: 0x0021e9 group: control font: IsabelleText |
356 \<^sup> code: 0x0021e7 group: control font: IsabelleText |
365 \<^sup> code: 0x0021e7 group: control font: IsabelleText |
357 \<^bold> code: 0x002759 group: control font: IsabelleText |
|
358 \<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_( |
366 \<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_( |
359 \<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_) |
367 \<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_) |
360 \<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^( |
368 \<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^( |
361 \<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^) |
369 \<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^) |
362 \<^smallskip> code: 0x002508 group: control |
|
363 \<^medskip> code: 0x002509 group: control |
|
364 \<^bigskip> code: 0x002501 group: control |
|
365 \<^item> code: 0x0025aa group: control |
|
366 \<^enum> code: 0x0025b8 group: control |
|