[isabelle-dev] NEWS

[Makarius]

* HOL: command 'typedef' now works within a local theory context -- 
without introducing dependencies on parameters or assumptions, which is 
not possible in Isabelle/Pure/HOL.  Note that the logical environment may 
contain multiple interpretations of local typedefs (with different 
non-emptiness proofs), even in a global theory context.