src/HOL/MiniML/README.html
changeset 14482 82774ac788ae
parent 14481 ab1e47451aaa
child 14483 6eac487f9cfa
--- a/src/HOL/MiniML/README.html	Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-<HTML><HEAD><TITLE>HOL/MiniML/README</TITLE></HEAD>
-<BODY>
-
-<H1>Type Inference for MiniML</H1>
-
-This theory defines the type inference rules and the type inference algorithm
-<em>W</em> for MiniML (simply-typed lambda terms with <tt>let</tt>) due to
-Milner. It proves the soundness and completeness of <em>W</em> w.r.t. the
-rules.
-
-<P>
-
-A report describing the theory is found here:<br>
-<A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W.html">
-Type Inference Verified: Algorithm <i>W</i> in Isabelle/HOL</A>.
-
-</BODY>
-</HTML>