diff -r 3eda95792083 -r c5cc02b56e0f src/HOL/Auth/document/root.tex
--- a/src/HOL/Auth/document/root.tex	Tue May 11 10:48:00 2004 +0200
+++ b/src/HOL/Auth/document/root.tex	Tue May 11 10:48:30 2004 +0200
@@ -1,5 +1,6 @@
 \documentclass[10pt,a4paper,twoside]{article}
 \usepackage{graphicx}
+\usepackage[latin1]{inputenc}
 \usepackage{latexsym,theorem}
 \usepackage{isabelle,isabellesym}
 \usepackage{pdfsetup}\urlstyle{rm}