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 "===>" = "===>" |
4 "===>" = "===>" |
5 |
5 |
|
6 "--->" = "\<midarrow>\<rightarrow>" |
|
7 |
6 (*HOL-NSA*) |
8 (*HOL-NSA*) |
7 "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" |
9 "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S" |
8 "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S" |
10 "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S" |