[isabelle-dev] NEWS: definitional typedef

[Makarius]

* The 'typedef' command has been upgraded from a partially checked
"axiomatization", to a full definitional specification that takes the
global collection of overloaded constant / type definitions into
account. Type definitions with open dependencies on overloaded
definitions need to be specified as "typedef (overloaded)". This
provides extra robustness in theory construction. Rare INCOMPATIBILITY.

* Command 'print_definitions' prints dependencies of definitional
specifications. This functionality used to be part of 'print_theory'.


This refers to 077b88f9ec16 .. 64a5bce1f498, the latter changeset also 
contains updated documentation in isar-ref.

I will come back to the isabelle-users thread "Isabelle Foundation & 
Certification" soon.  There is no need to add to the confusion by 
cross-posting on isabelle-dev.


 	Makarius