359 \<newline> code: 0x0023ce |
359 \<newline> code: 0x0023ce |
360 \<comment> code: 0x002015 font: IsabelleText |
360 \<comment> code: 0x002015 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 group: control font: IsabelleText |
364 \<^undefined> code: 0x002756 font: IsabelleText |
365 \<^noindent> code: 0x0021e4 group: control font: IsabelleText |
365 \<^noindent> code: 0x0021e4 group: document font: IsabelleText |
366 \<^smallskip> code: 0x002508 group: control font: IsabelleText |
366 \<^smallskip> code: 0x002508 group: document font: IsabelleText |
367 \<^medskip> code: 0x002509 group: control font: IsabelleText |
367 \<^medskip> code: 0x002509 group: document font: IsabelleText |
368 \<^bigskip> code: 0x002501 group: control font: IsabelleText |
368 \<^bigskip> code: 0x002501 group: document font: IsabelleText |
369 \<^item> code: 0x0025aa group: control font: IsabelleText |
369 \<^item> code: 0x0025aa group: document font: IsabelleText |
370 \<^enum> code: 0x0025b8 group: control font: IsabelleText |
370 \<^enum> code: 0x0025b8 group: document font: IsabelleText |
371 \<^descr> code: 0x0027a7 group: control font: IsabelleText |
371 \<^descr> code: 0x0027a7 group: document font: IsabelleText |
372 \<^footnote> code: 0x00204b group: control font: IsabelleText |
372 \<^footnote> code: 0x00204b group: document font: IsabelleText |
373 \<^verbatim> code: 0x0025a9 group: control font: IsabelleText |
373 \<^verbatim> code: 0x0025a9 group: document font: IsabelleText |
374 \<^theory_text> code: 0x002b1a group: control font: IsabelleText |
374 \<^theory_text> code: 0x002b1a group: document font: IsabelleText |
375 \<^emph> code: 0x002217 group: control font: IsabelleText |
375 \<^emph> code: 0x002217 group: document font: IsabelleText |
376 \<^bold> code: 0x002759 group: control font: IsabelleText |
376 \<^bold> code: 0x002759 group: control group: document font: IsabelleText |
377 \<^sub> code: 0x0021e9 group: control font: IsabelleText |
377 \<^sub> code: 0x0021e9 group: control font: IsabelleText |
378 \<^sup> code: 0x0021e7 group: control font: IsabelleText |
378 \<^sup> code: 0x0021e7 group: control font: IsabelleText |
379 \<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_( |
379 \<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_( |
380 \<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_) |
380 \<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_) |
381 \<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^( |
381 \<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^( |