NEWS is not just for bad news -- infamous INCOMPATIBILITY entries -- but for any "user-relevant changes". If things are not user-relevant then what is the point of doing them in the first place?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
