diff -r 7dfc3c217414 -r 88e0d3160909 src/HOL/MiniML/README.html
--- a/src/HOL/MiniML/README.html Tue May 21 10:50:40 1996 +0200
+++ b/src/HOL/MiniML/README.html Tue May 21 10:52:26 1996 +0200
@@ -6,7 +6,7 @@
This theory defines the type inference rules and the type inference algorithm
*W* for simply-typed lambda terms due to Milner. It proves the
soundness and completeness of *W* w.r.t. to the rules. An optimized
-version *I* is shown equivalent to *W* (one direction only).
+version *I* is shown to implement *W*.