| changeset 27191 | 0fe5b95797da |
| parent 27145 | 0337828b7815 |
| child 27200 | 00b7b55b61bd |
--- a/NEWS Fri Jun 13 20:57:51 2008 +0200 +++ b/NEWS Fri Jun 13 21:04:07 2008 +0200 @@ -6,6 +6,10 @@ *** Pure *** +* Recovered hiding of consts, which was accidentally broken in +Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really +makes c inaccessible; consider using ``hide (open) const c'' instead. + * Command 'instance': attached definitions now longer accepted. INCOMPATIBILITY, use proper 'instantiation' target.