[isabelle-dev] NEWS: simplified typedef

Makarius makarius at sketis.net
Fri Oct 12 21:57:35 CEST 2012

* Simplified 'typedef' specifications: historical options for implicit
set definition and alternative name have been discontinued.  The
former behavior of "typedef (open) t = A" is now the default, but
written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories

This refers to Isabelle/c13b39542972.


More information about the isabelle-dev mailing list