Summary
- prefer infix operations;
- structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
- proper signature;
- tuned signature;
- tuned;
- tuned signature;
- proper type; tuned;
- careful export of type-dependent functions, without losing their special status;
- clarified modules;
- clarified modules;