equal
deleted
inserted
replaced
1 (* additional abbreviations for syntactic completion *) |
1 (* additional abbreviations for syntactic completion *) |
2 |
2 |
3 (*prevent replacement of very long arrows*) |
3 (*prevent replacement of very long arrows*) |
4 "--->" = "--->" |
|
5 "---->" = "---->" |
|
6 "----->" = "----->" |
|
7 "===>" = "===>" |
4 "===>" = "===>" |
8 |
5 |
9 (*HOL-NSA*) |
6 (*HOL-NSA*) |
10 "---->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" |
7 "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" |
11 "---->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S" |
8 "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S" |