diff -r e893e45219c3 -r 6ec40bc934e1 NEWS --- a/NEWS Fri Jul 02 10:45:25 2010 +0200 +++ b/NEWS Fri Jul 02 10:47:50 2010 +0200 @@ -18,7 +18,7 @@ *** HOL *** * Abolished symbol type names: "prod" and "sum" replace "*" and "+" -respectively. INCOMPATBILITY. +respectively. INCOMPATIBILITY. * Constant "split" has been merged with constant "prod_case"; names of ML functions, facts etc. involving split have been retained so far,