# HG changeset patch
# User wenzelm
# Date 1207766804 -7200
# Node ID 9114b5fe533a0a914f0f1fe5b96f798dea04d571
# Parent  43cb72871897c07b46824335488f7c2bf9694692
\usepackage[english]{babel} (required for guillemots);

diff -r 43cb72871897 -r 9114b5fe533a src/HOL/Library/Library/document/root.tex
--- a/src/HOL/Library/Library/document/root.tex	Wed Apr 09 17:46:17 2008 +0200
+++ b/src/HOL/Library/Library/document/root.tex	Wed Apr 09 20:46:44 2008 +0200
@@ -4,6 +4,7 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{ifthen}
 \usepackage[latin1]{inputenc}
+\usepackage[english]{babel}
 \usepackage{isabelle,isabellesym,amssymb}
 \usepackage{pdfsetup}