[isabelle-dev] NEWS: definitional typedef
makarius at sketis.net
Sat Sep 26 00:13:37 CEST 2015
* 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.
More information about the isabelle-dev