# HG changeset patch
# User wenzelm
# Date 1268489567 -3600
# Node ID 1416f568b2b62b86fe73b662d11aa670c44e5ee7
# Parent  93603d7b8ee96be54be58d52e156a3b1054f9087
command 'typedef' now works within a local theory context;

diff -r 93603d7b8ee9 -r 1416f568b2b6 NEWS
--- 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.