# HG changeset patch
# User wenzelm
# Date 1396532431 -7200
# Node ID c771f0fe28d14d058e8ed827a4cfc088b37ef1e2
# Parent  d92eb5c3960db2da463e9c54753d9550d9211665
more symbol abbrevs, e.g. relevant for list comprehension in HOL/List.thy or HOL/Library/Monad_Syntax.thy;

diff -r d92eb5c3960d -r c771f0fe28d1 etc/symbols
--- a/etc/symbols	Thu Apr 03 14:54:17 2014 +0200
+++ b/etc/symbols	Thu Apr 03 15:40:31 2014 +0200
@@ -154,7 +154,7 @@
 \<rat>                  code: 0x00211a  group: letter
 \<real>                 code: 0x00211d  group: letter
 \<int>                  code: 0x002124  group: letter
-\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
+\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.  abbrev: <-
 \<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
 \<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
 \<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->