--- a/NEWS Sat Mar 13 15:12:17 2010 +0100
+++ b/NEWS Sat Mar 13 15:12:47 2010 +0100
@@ -83,6 +83,12 @@
*** 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.
+
* Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
Min, Max from theory Finite_Set. INCOMPATIBILITY.