src/HOL/MiniML/README.html
changeset 2531 7cfa1a9c744d
parent 2523 0ccea141409b
equal deleted inserted replaced
2530:02ccf78ad0a3 2531:7cfa1a9c744d
     2 <BODY>
     2 <BODY>
     3 
     3 
     4 <H1>Type Inference for MiniML</H1>
     4 <H1>Type Inference for MiniML</H1>
     5 
     5 
     6 This theory defines the type inference rules and the type inference algorithm
     6 This theory defines the type inference rules and the type inference algorithm
     7 <em>W</em> for simply-typed lambda terms due to Milner. It proves the
     7 <em>W</em> for MiniML (simply-typed lambda terms with <tt>let</tt>) due to
     8 soundness and completeness of <em>W</em> w.r.t. to the rules.
     8 Milner. It proves the soundness and completeness of <em>W</em> w.r.t. the
       
     9 rules.
     9 
    10 
    10 <P>
    11 <P>
    11 
    12 
    12 A report describing the theory is found here:<br>
    13 A report describing the theory is found here:<br>
    13 <A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W.html">
    14 <A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W.html">