etc/symbols
changeset 70066 6dc5506ad449
parent 69371 0d84e3db67c2
child 70072 def3ec9cdb7e
     1.1 --- a/etc/symbols	Sat Mar 09 13:24:59 2019 +0100
     1.2 +++ b/etc/symbols	Sat Mar 09 13:35:49 2019 +0100
     1.3 @@ -359,6 +359,7 @@
     1.4  \<hole>                 code: 0x002311
     1.5  \<newline>              code: 0x0023ce
     1.6  \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     1.7 +\<marker>               code: 0x002710  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     1.8  \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: Isabelle␣DejaVu␣Sans␣Mono
     1.9  \<^latex>                               group: document  argument: cartouche
    1.10  \<open>                 code: 0x002039  group: punctuation  font: Isabelle␣DejaVu␣Sans␣Mono  abbrev: <<