NEWS
changeset 61969 e01015e49041
parent 61964 37a0cbee00c2
child 61970 6226261144d7
equal deleted inserted replaced
61968:e13e70f32407 61969:e01015e49041
   499 
   499 
   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 
       
   505   notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
   504 
   506 
   505 * The alternative notation "\<Colon>" for type and sort constraints has been
   507 * The alternative notation "\<Colon>" for type and sort constraints has been
   506 removed: in LaTeX document output it looks the same as "::".
   508 removed: in LaTeX document output it looks the same as "::".
   507 INCOMPATIBILITY, use plain "::" instead.
   509 INCOMPATIBILITY, use plain "::" instead.
   508 
   510