etc/symbols
changeset 61405 d2ce32c5793a
parent 59974 b911c8ba0b69
child 61437 8bb17fd2fa81
--- a/etc/symbols	Mon Oct 12 17:06:49 2015 +0200
+++ b/etc/symbols	Mon Oct 12 17:10:36 2015 +0200
@@ -359,3 +359,8 @@
 \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
 \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
 \<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
+\<^smallskip>           code: 0x002508  group: control
+\<^medskip>             code: 0x002509  group: control
+\<^bigskip>             code: 0x002501  group: control
+\<^item>                code: 0x0025aa  group: control
+\<^enum>                code: 0x0025b8  group: control