| changeset 55033 | 8e8243975860 |
| parent 55015 | e33c5bd729ff |
| child 55044 | 5f4d5f6876f1 |
--- a/etc/symbols Fri Jan 17 20:51:36 2014 +0100 +++ b/etc/symbols Sat Jan 18 19:15:12 2014 +0100 @@ -348,6 +348,8 @@ \<hungarumlaut> code: 0x0002dd \<some> code: 0x0003f5 \<newline> code: 0x0023ce +\<open> code: 0x002039 abbrev: << font: IsabelleText +\<close> code: 0x00203a abbrev: >> font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText