author | wenzelm |
Thu, 05 Nov 2015 10:35:37 +0100 | |
changeset 61584 | f06e5a5a4b46 |
parent 61583 | c2b7033fa0ba |
child 61585 | a9599d3d7610 |
etc/symbols | file | annotate | diff | comparison | revisions |
--- a/etc/symbols Thu Nov 05 10:34:34 2015 +0100 +++ b/etc/symbols Thu Nov 05 10:35:37 2015 +0100 @@ -348,7 +348,7 @@ \<some> code: 0x0003f5 \<hole> code: 0x002311 \<newline> code: 0x0023ce -\<comment> code: 0x002015 +\<comment> code: 0x002015 font: IsabelleText \<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: << \<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \<here> code: 0x002302 font: IsabelleText