[isabelle-dev] NEWS

Makarius makarius at sketis.net
Sat Mar 13 17:27:59 CET 2010


* 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.



More information about the isabelle-dev mailing list