changeset 61579 | 634cd44bb1d3 |
parent 61571 | 9c50eb3bff50 |
child 61584 | f06e5a5a4b46 |
--- a/etc/symbols Wed Nov 04 23:27:00 2015 +0100 +++ b/etc/symbols Thu Nov 05 00:02:30 2015 +0100 @@ -348,6 +348,7 @@ \<some> code: 0x0003f5 \<hole> code: 0x002311 \<newline> code: 0x0023ce +\<comment> code: 0x002015 \<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: << \<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \<here> code: 0x002302 font: IsabelleText