NEWS
changeset 66480 4b8d1df8933b
parent 66474 3ff851a8cb4b
child 66481 d35f7a9f92e2
equal deleted inserted replaced
66479:5c0a3f63057d 66480:4b8d1df8933b
   213 the literature. Minor INCOMPATIBILITY.
   213 the literature. Minor INCOMPATIBILITY.
   214 
   214 
   215 * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
   215 * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
   216 been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
   216 been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
   217 
   217 
   218 * Theory "HOL-Library.Formal_Power_Series": constants E/L/F have been
   218 * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
   219 renamed to fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
   219 renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name
   220 space. INCOMPATIBILITY.
   220 space. INCOMPATIBILITY.
   221 
   221 
   222 * Theory "HOL-Library.FinFun" has been moved to AFP (again).
   222 * Theory "HOL-Library.FinFun" has been moved to AFP (again).
   223 INCOMPATIBILITY.
   223 INCOMPATIBILITY.
   224 
   224