tuned comments;
authorwenzelm
Wed Jan 16 11:31:08 2013 +0100 (2013-01-16)
changeset 5091054f06ba192ef
parent 50909 b2fb1ab1475d
child 50911 ee7fe4230642
tuned comments;
src/Pure/ML-Systems/compiler_polyml.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/install_pp_polyml.ML
src/Pure/ML/ml_compiler_polyml.ML
     1.1 --- a/src/Pure/ML-Systems/compiler_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
     1.2 +++ b/src/Pure/ML-Systems/compiler_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
     1.3 @@ -1,8 +1,6 @@
     1.4  (*  Title:      Pure/ML-Systems/compiler_polyml.ML
     1.5  
     1.6 -Runtime compilation for Poly/ML 5.3.0 or later.
     1.7 -
     1.8 -See also Pure/ML/ml_compiler_polyml.ML for advanced version.
     1.9 +Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
    1.10  *)
    1.11  
    1.12  local
     2.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
     2.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      Pure/ML-Systems/multithreading_polyml.ML
     2.5      Author:     Makarius
     2.6  
     2.7 -Multithreading in Poly/ML 5.3.0 or later (cf. polyml/basis/Thread.sml).
     2.8 +Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
     2.9  *)
    2.10  
    2.11  signature MULTITHREADING_POLYML =
     3.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 11:25:26 2013 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 11:31:08 2013 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      Pure/ML-Systems/polyml.ML
     3.5      Author:     Makarius
     3.6  
     3.7 -Compatibility wrapper for Poly/ML 5.3.0 or later.
     3.8 +Compatibility wrapper for Poly/ML.
     3.9  *)
    3.10  
    3.11  (* exceptions *)
     4.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 11:25:26 2013 +0100
     4.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 11:31:08 2013 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4  (*  Title:      Pure/ML-Systems/smlnj.ML
     4.5  
     4.6 -Compatibility file for Standard ML of New Jersey 110 or later.
     4.7 +Compatibility file for Standard ML of New Jersey.
     4.8  *)
     4.9  
    4.10  use "ML-Systems/proper_int.ML";
     5.1 --- a/src/Pure/ML/install_pp_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
     5.2 +++ b/src/Pure/ML/install_pp_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
     5.3 @@ -1,7 +1,7 @@
     5.4  (*  Title:      Pure/ML/install_pp_polyml.ML
     5.5      Author:     Makarius
     5.6  
     5.7 -Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
     5.8 +Extra toplevel pretty-printing for Poly/ML.
     5.9  *)
    5.10  
    5.11  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
     6.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 11:25:26 2013 +0100
     6.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
     6.3 @@ -1,7 +1,7 @@
     6.4  (*  Title:      Pure/ML/ml_compiler_polyml.ML
     6.5      Author:     Makarius
     6.6  
     6.7 -Advanced runtime compilation for Poly/ML 5.3.0 or later.
     6.8 +Advanced runtime compilation for Poly/ML.
     6.9  *)
    6.10  
    6.11  structure ML_Compiler: ML_COMPILER =