[isabelle-dev] structure PolyML sealed after bootstrap

Makarius makarius at sketis.net
Sun Apr 3 00:13:19 CEST 2016

See Isabelle/e6e80a8bf624.

There is no NEWS entry, because this is strictly speaking not 
user-relevant: structure PolyML belongs to the system implementation and 
was never officially available in Isabelle/ML user space.

Anything that is required from it needs to be provided by suitable 
Isabelle/ML modules, e.g. ML_System.obj_size.

If I've forgotten anything important, please say so -- before the next 


More information about the isabelle-dev mailing list