\usepackage[english]{babel} (required for guillemots);

--- 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}