equal
deleted
inserted
replaced
500 notation Omega_Words_Fun.conc (infixr "conc" 65) |
500 notation Omega_Words_Fun.conc (infixr "conc" 65) |
501 |
501 |
502 notation Preorder.equiv ("op ~~") |
502 notation Preorder.equiv ("op ~~") |
503 and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) |
503 and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) |
504 |
504 |
|
505 notation (in topological_space) tendsto (infixr "--->" 55) |
505 notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) |
506 notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) |
506 |
507 |
507 notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) |
508 notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) |
508 notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
509 notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
509 |
510 |