author | wenzelm |
Tue, 19 Apr 2016 15:53:12 +0200 | |
changeset 63029 | 8b830d2bf94c |
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" |