# HG changeset patch
# User wenzelm
# Date 1393518256 -3600
# Node ID 96861130f922ebdcc23f76c226f6adcb8953bdf0
# Parent  3086f57e48e9a6a353105dde3fa435e33d9dd957
more symbol abbrevs to support HOL library maintenance;

diff -r 3086f57e48e9 -r 96861130f922 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