Added lecture notes by Matthes and Loader.

--- a/src/HOL/Lambda/document/root.bib	Thu Sep 06 11:48:51 2007 +0200
+++ b/src/HOL/Lambda/document/root.bib	Thu Sep 06 11:50:32 2007 +0200
@@ -1,3 +1,24 @@
+@TechReport{Loader1998,
+  author =	 {Ralph Loader},
+  title =	 {{N}otes on {S}imply {T}yped {L}ambda {C}alculus},
+  institution =	 {Laboratory for Foundations of Computer Science,
+                  School of Informatics, University of Edinburgh},
+  year =	 1998,
+  number =	 {ECS-LFCS-98-381}
+}
+
+@InProceedings{Matthes-ESSLLI2000,
+  author =	 {Ralph Matthes},
+  title =	 {{L}ambda {C}alculus: {A} {C}ase for {I}nductive
+                  {D}efinitions},
+  booktitle =	 {Lecture notes of the 12th European Summer School in
+                  Logic, Language and Information (ESSLLI 2000)},
+  year =	 2000,
+  month =	 {August},
+  publisher =	 {School of Computer Science, University of
+                  Birmingham}
+}
+
 @Article{Matthes-Joachimski-AML,
   author =       {Felix Joachimski and Ralph Matthes},
   title =        {Short Proofs of Normalization for the simply-typed