2016-04-02 agoprefer infix operations;
wenzelm [Sat, 02 Apr 2016 23:29:05 +0200] rev 62826
prefer infix operations;

2016-04-02 agostructure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm [Sat, 02 Apr 2016 23:14:08 +0200] rev 62825
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;

2016-04-02 agoproper signature;
wenzelm [Sat, 02 Apr 2016 22:46:12 +0200] rev 62824
proper signature;

2016-04-02 agotuned signature;
wenzelm [Sat, 02 Apr 2016 22:38:26 +0200] rev 62823
tuned signature;

2016-04-02 agotuned;
wenzelm [Sat, 02 Apr 2016 22:13:00 +0200] rev 62822
tuned;

2016-04-02 agotuned signature;
wenzelm [Sat, 02 Apr 2016 21:55:32 +0200] rev 62821
tuned signature;

2016-04-02 agoproper type;
wenzelm [Sat, 02 Apr 2016 21:54:51 +0200] rev 62820
proper type;
tuned;

2016-04-02 agocareful export of type-dependent functions, without losing their special status;
wenzelm [Sat, 02 Apr 2016 21:10:07 +0200] rev 62819
careful export of type-dependent functions, without losing their special status;

2016-04-02 agoclarified modules;
wenzelm [Sat, 02 Apr 2016 20:33:34 +0200] rev 62818
clarified modules;

2016-04-02 agoclarified modules;
wenzelm [Sat, 02 Apr 2016 20:23:51 +0200] rev 62817
clarified modules;