\usepackage{textcomp};

--- a/src/HOL/ex/document/root.tex	Tue Dec 04 02:01:49 2001 +0100
+++ b/src/HOL/ex/document/root.tex	Tue Dec 04 02:02:10 2001 +0100
@@ -4,6 +4,7 @@
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage[english]{babel}
+\usepackage{textcomp}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}