author | wenzelm |
Mon, 01 Jun 2009 23:28:02 +0200 | |
changeset 31329 | c8821a6297f9 |
parent 31328 | 0d3aa0aeb96f |
child 31330 | 7bfbd0e07a40 |
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Mon Jun 01 16:12:42 2009 +0200 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Mon Jun 01 23:28:02 2009 +0200 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/compiler_polyml-5.0.ML -Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1. +Runtime compilation for Poly/ML 5.0 and 5.1. *) fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =