# HG changeset patch
# User wenzelm
# Date 1451429444 -3600
# Node ID a70b89a3e02ec0fd82549339ec18cd8ff061136d
# Parent  720fa884656e7d67e4372f3f8c94b2d35c210602
simplified abbrevs: exploit ambiguity;

diff -r 720fa884656e -r a70b89a3e02e etc/abbrevs
--- a/etc/abbrevs	Tue Dec 29 23:40:04 2015 +0100
+++ b/etc/abbrevs	Tue Dec 29 23:50:44 2015 +0100
@@ -1,11 +1,8 @@
 (* additional abbreviations for syntactic completion *)
 
 (*prevent replacement of very long arrows*)
-"--->" = "--->"
-"---->" = "---->"
-"----->" = "----->"
 "===>" = "===>"
 
 (*HOL-NSA*)
-"---->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
-"---->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
+"--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
+"--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
diff -r 720fa884656e -r a70b89a3e02e etc/symbols
--- a/etc/symbols	Tue Dec 29 23:40:04 2015 +0100
+++ b/etc/symbols	Tue Dec 29 23:50:44 2015 +0100
@@ -161,7 +161,7 @@
 \<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
 \<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->
 \<longlongrightarrow>   code: 0x00290f  group: arrow  abbrev: .>  abbrev: --->
-\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: ---->
+\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: --->
 \<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
 \<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
 \<Lleftarrow>           code: 0x0021da  group: arrow  abbrev: <.