NEWS
changeset 35745 1416f568b2b6
parent 35728 c36ade6f4c33
child 35763 765f8adf10f9
--- 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.