# HG changeset patch
# User wenzelm
# Date 1010952807 -3600
# Node ID b0b012b11a36e3b39b3237216a0f4b38b38816a7
# Parent  80f10551fb5941006e1a36407799cef61d0ac165
\usepackage[latin1]{inputenc};

diff -r 80f10551fb59 -r b0b012b11a36 src/HOL/document/root.tex
--- a/src/HOL/document/root.tex	Sun Jan 13 21:12:43 2002 +0100
+++ b/src/HOL/document/root.tex	Sun Jan 13 21:13:27 2002 +0100
@@ -3,6 +3,7 @@
 
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage[latin1]{inputenc}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}