equal
deleted
inserted
replaced
383 \<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^) |
383 \<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^) |
384 \<^file> code: 0x01F5CF group: icon font: IsabelleText |
384 \<^file> code: 0x01F5CF group: icon font: IsabelleText |
385 \<^dir> code: 0x01F5C0 group: icon font: IsabelleText |
385 \<^dir> code: 0x01F5C0 group: icon font: IsabelleText |
386 \<^url> code: 0x01F310 group: icon font: IsabelleText |
386 \<^url> code: 0x01F310 group: icon font: IsabelleText |
387 \<^doc> code: 0x01F4D3 group: icon font: IsabelleText |
387 \<^doc> code: 0x01F4D3 group: icon font: IsabelleText |
|
388 \<^action> code: 0x00261b group: icon font: IsabelleText |