#125 (Apr 2, 2016, 11:56:11 PM)

1. prefer infix operations; (detail / hgweb)
2. structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; (detail / hgweb)
3. proper signature; (detail / hgweb)
4. tuned signature; (detail / hgweb)
5. tuned; (detail / hgweb)
6. tuned signature; (detail / hgweb)
7. proper type;
   tuned; (detail / hgweb)
8. careful export of type-dependent functions, without losing their special status; (detail / hgweb)
9. clarified modules; (detail / hgweb)
10. clarified modules; (detail / hgweb)

Started by an SCM change