| changeset 63579 | 73939a9b70a3 |
| parent 61976 | 3a27957ac658 |
| 63578:e8990d0e3965 | 63579:73939a9b70a3 |
|---|---|
2 |
2 |
3 (*prevent replacement of very long arrows*) |
3 (*prevent replacement of very long arrows*) |
4 "===>" = "===>" |
4 "===>" = "===>" |
5 |
5 |
6 "--->" = "\<midarrow>\<rightarrow>" |
6 "--->" = "\<midarrow>\<rightarrow>" |
7 |
|
8 (*HOL-NSA*) |
|
9 "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" |
|
10 "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S" |