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