equal
deleted
inserted
replaced
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: IsabelleText |
362 \<^cancel> code: 0x002326 group: document argument: cartouche font: IsabelleText |
362 \<^cancel> code: 0x002326 group: document argument: cartouche font: IsabelleText |
|
363 \<^latex> group: document argument: cartouche |
363 \<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: << |
364 \<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: << |
364 \<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >> |
365 \<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >> |
365 \<^here> code: 0x002302 font: IsabelleText |
366 \<^here> code: 0x002302 font: IsabelleText |
366 \<^undefined> code: 0x002756 font: IsabelleText |
367 \<^undefined> code: 0x002756 font: IsabelleText |
367 \<^noindent> code: 0x0021e4 group: document font: IsabelleText |
368 \<^noindent> code: 0x0021e4 group: document font: IsabelleText |