diff -r 8648c6651f07 -r d4866f6ff2f9 doc-src/Tutorial/tutorial.tex
--- a/doc-src/Tutorial/tutorial.tex	Tue Jan 12 15:40:53 1999 +0100
+++ b/doc-src/Tutorial/tutorial.tex	Tue Jan 12 15:48:59 1999 +0100
@@ -1,5 +1,5 @@
 \documentclass[11pt]{report}
-\usepackage{a4,latexsym,moreverb}
+\usepackage{a4,latexsym,verbatim}
 \usepackage{graphicx}
 
 \makeatletter
@@ -54,9 +54,9 @@
 \subsubsection*{Acknowledgements}
 This tutorial owes a lot to the constant discussions with and the valuable
 feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
-Wolfgang Naraschewski, David von Oheimb, Leonor Prensa-Nieto, Cornelia Pusch
-and Markus Wenzel. Stefan Merz was also kind enough to read and comment on a
-draft version.
+Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
+and Markus Wenzel. Stefan Berghofer and Stefan Merz were also kind enough to
+read and comment on a draft version.
 \clearfirst
 
 \input{basics}