diff -r 928156a95e1a -r 4538153bcc5c NEWS --- a/NEWS Sun Feb 26 11:38:33 2017 +0100 +++ b/NEWS Sun Feb 26 13:22:14 2017 +0100 @@ -45,6 +45,8 @@ *** HOL *** +* Theory Library/FinFun has been moved to AFP (again). INCOMPATIBILITY. + * Some old and rarely used ASCII replacement syntax has been removed. INCOMPATIBILITY, standard syntax with symbols should be used instead. The subsequent commands help to reproduce the old forms, e.g. to