| author | wenzelm | 
| Thu, 26 May 2016 16:57:14 +0200 | |
| changeset 63166 | 143f58bb34f9 | 
| parent 61976 | 3a27957ac658 | 
| child 63579 | 73939a9b70a3 | 
| permissions | -rw-r--r-- | 
| 61961 | 1 | (* additional abbreviations for syntactic completion *) | 
| 2 | ||
| 3 | (*prevent replacement of very long arrows*) | |
| 4 | "===>" = "===>" | |
| 61970 | 5 | |
| 61976 | 6 | "--->" = "\<midarrow>\<rightarrow>" | 
| 7 | ||
| 61970 | 8 | (*HOL-NSA*) | 
| 61972 | 9 | "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" | 
| 10 | "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S" |