--- a/src/HOL/Isar_examples/W_correct.thy Thu Oct 28 19:53:24 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy Thu Oct 28 19:57:34 1999 +0200
@@ -3,13 +3,17 @@
Author: Markus Wenzel, TU Muenchen
Correctness of Milner's type inference algorithm W (let-free version).
-Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow.
*)
header {* Milner's type inference algorithm~W (let-free version) *};
theory W_correct = Main + Type:;
+text_raw {*
+ \footnote{Based upon \url{http://isabelle.in.tum.de/library/HOL/W0}
+ by Dieter Nazareth and Tobias Nipkow.}
+*};
+
subsection "Mini ML with type inference rules";