--- 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"
--- 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: <.