\usepackage[latin1]{inputenc};

--- a/src/HOL/ex/document/root.tex	Fri Dec 14 22:27:58 2001 +0100
+++ b/src/HOL/ex/document/root.tex	Fri Dec 14 22:28:13 2001 +0100
@@ -3,6 +3,7 @@
 
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
+\usepackage[latin1]{inputenc}
 \usepackage[english]{babel}
 \usepackage{textcomp}
 \usepackage{pdfsetup}