more symbol abbrevs to support HOL library maintenance;
authorwenzelm
Thu, 27 Feb 2014 17:24:16 +0100
changeset 55786 96861130f922
parent 55785 3086f57e48e9
child 55787 41a73a41f6c8
more symbol abbrevs to support HOL library maintenance;
etc/symbols
--- a/etc/symbols	Thu Feb 27 14:51:14 2014 +0100
+++ b/etc/symbols	Thu Feb 27 17:24:16 2014 +0100
@@ -272,7 +272,7 @@
 \<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
 \<plusminus>            code: 0x0000b1  group: operator
 \<minusplus>            code: 0x002213  group: operator
-\<times>                code: 0x0000d7  group: operator
+\<times>                code: 0x0000d7  group: operator  abbrev: <*>
 \<div>                  code: 0x0000f7  group: operator
 \<cdot>                 code: 0x0022c5  group: operator
 \<star>                 code: 0x0022c6  group: operator