src/HOL/Proofs/Lambda/document/root.bib

clarified example settings for Proof General;

@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
                  $\lambda$-calculus, permutative conversions and
                  {G}{\"o}del's {T}},
  journal =      {Archive for Mathematical Logic},
  year =         2003,
  volume =       42,
  number =       1,
  pages =        {59--87}
}

@Article{Takahashi-IandC,
  author = 	 {Masako Takahashi},
  title = 	 {Parallel reductions in $\lambda$-calculus},
  journal = 	 {Information and Computation},
  year = 	 1995,
  volume =	 118,
  number =	 1,
  pages =	 {120--127},
  month =	 {April}
}