changeset 61970 | 6226261144d7 |
parent 61968 | e13e70f32407 |
child 61971 | 720fa884656e |
61969:e01015e49041 | 61970:6226261144d7 |
---|---|
3 (*prevent replacement of very long arrows*) |
3 (*prevent replacement of very long arrows*) |
4 "--->" = "--->" |
4 "--->" = "--->" |
5 "---->" = "---->" |
5 "---->" = "---->" |
6 "----->" = "----->" |
6 "----->" = "----->" |
7 "===>" = "===>" |
7 "===>" = "===>" |
8 |
|
9 (*HOL-NSA*) |
|
10 "---->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" |