| author | nipkow | 
| Tue, 21 May 1996 10:52:26 +0200 | |
| changeset 1753 | 88e0d3160909 | 
| parent 1752 | 7dfc3c217414 | 
| child 1754 | 852093aeb0ab | 
--- 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 <em>W</em> for simply-typed lambda terms due to Milner. It proves the soundness and completeness of <em>W</em> w.r.t. to the rules. An optimized -version <em>I</em> is shown equivalent to <em>W</em> (one direction only). +version <em>I</em> is shown to implement <em>W</em>. <P>