src/HOL/Isar_examples/W_correct.thy
changeset 7968 964b65b4e433
parent 7809 c3e6f27bfcb7
child 7982 d534b897ce39
     1.1 --- a/src/HOL/Isar_examples/W_correct.thy	Thu Oct 28 19:53:24 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/W_correct.thy	Thu Oct 28 19:57:34 1999 +0200
     1.3 @@ -3,13 +3,17 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Correctness of Milner's type inference algorithm W (let-free version).
     1.7 -Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow.
     1.8  *)
     1.9  
    1.10  header {* Milner's type inference algorithm~W (let-free version) *};
    1.11  
    1.12  theory W_correct = Main + Type:;
    1.13  
    1.14 +text_raw {*
    1.15 +  \footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0}
    1.16 +  by Dieter Nazareth and Tobias Nipkow.}
    1.17 +*};
    1.18 +
    1.19  
    1.20  subsection "Mini ML with type inference rules";
    1.21