\usepackage[latin1]{inputenc};
authorwenzelm
Sun Jan 13 21:13:27 2002 +0100 (2002-01-13)
changeset 12737b0b012b11a36
parent 12736 80f10551fb59
child 12738 9d80e3746eb0
\usepackage[latin1]{inputenc};
src/HOL/document/root.tex
     1.1 --- a/src/HOL/document/root.tex	Sun Jan 13 21:12:43 2002 +0100
     1.2 +++ b/src/HOL/document/root.tex	Sun Jan 13 21:13:27 2002 +0100
     1.3 @@ -3,6 +3,7 @@
     1.4  
     1.5  \documentclass[11pt,a4paper]{article}
     1.6  \usepackage{graphicx,isabelle,isabellesym,latexsym}
     1.7 +\usepackage[latin1]{inputenc}
     1.8  \usepackage{pdfsetup}
     1.9  
    1.10  \urlstyle{rm}