tuned comments;
authorwenzelm
Sun, 10 Apr 2016 22:27:05 +0200
changeset 62945 c38c08889aa9
parent 62944 3ee643c5ed00
child 62946 9f537dd83677
tuned comments;
src/Pure/General/socket_io.ML
src/Pure/ML/ml_profiling.ML
src/Pure/ML/ml_statistics.ML
--- a/src/Pure/General/socket_io.ML	Sun Apr 10 21:46:12 2016 +0200
+++ b/src/Pure/General/socket_io.ML	Sun Apr 10 22:27:05 2016 +0200
@@ -4,8 +4,6 @@
 
 Stream IO over TCP sockets.  Following example 10.2 in "The Standard
 ML Basis Library" by Emden R. Gansner and John H. Reppy.
-
-Note: BinIO requires Poly/ML 5.5.x to work reliably.
 *)
 
 signature SOCKET_IO =
--- a/src/Pure/ML/ml_profiling.ML	Sun Apr 10 21:46:12 2016 +0200
+++ b/src/Pure/ML/ml_profiling.ML	Sun Apr 10 22:27:05 2016 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_profiling.ML
     Author:     Makarius
 
-Profiling for Poly/ML 5.6.
+ML profiling.
 *)
 
 signature ML_PROFILING =
--- a/src/Pure/ML/ml_statistics.ML	Sun Apr 10 21:46:12 2016 +0200
+++ b/src/Pure/ML/ml_statistics.ML	Sun Apr 10 22:27:05 2016 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_statistics.ML
     Author:     Makarius
 
-ML runtime statistics for Poly/ML 5.5.0 or later.
+ML runtime statistics.
 *)
 
 signature ML_STATISTICS =