# HG changeset patch
# User wenzelm
# Date 1008084331 -3600
# Node ID d3577f7e26bfc9b7692075705b0932be7372a146
# Parent  79b188f6d0aea72d3dca571acaa0804e8f5c127d
tuned;

diff -r 79b188f6d0ae -r d3577f7e26bf src/HOL/Library/document/root.tex
--- a/src/HOL/Library/document/root.tex	Tue Dec 11 16:22:44 2001 +0100
+++ b/src/HOL/Library/document/root.tex	Tue Dec 11 16:25:31 2001 +0100
@@ -15,7 +15,7 @@
 \author{
   Gertrud Bauer \\
   Tobias Nipkow \\
-  David von Oheimb\\
+  David von Oheimb \\
   Lawrence C Paulson \\
   Thomas M Rasmussen \\
   Christophe Tabacznyj \\