| changeset 61976 | 3a27957ac658 |
| parent 61972 | a70b89a3e02e |
| child 63579 | 73939a9b70a3 |
--- a/etc/abbrevs Wed Dec 30 11:37:29 2015 +0100 +++ b/etc/abbrevs Wed Dec 30 14:05:51 2015 +0100 @@ -3,6 +3,8 @@ (*prevent replacement of very long arrows*) "===>" = "===>" +"--->" = "\<midarrow>\<rightarrow>" + (*HOL-NSA*) "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"