etc/abbrevs
changeset 61970 6226261144d7
parent 61968 e13e70f32407
child 61971 720fa884656e
equal deleted inserted replaced
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"