\usepackage{amssymb};

--- a/src/HOL/ex/document/root.tex	Sun Feb 12 12:29:01 2006 +0100
+++ b/src/HOL/ex/document/root.tex	Sun Feb 12 20:32:59 2006 +0100
@@ -6,6 +6,7 @@
 \usepackage[latin1]{inputenc}
 \usepackage[english]{babel}
 \usepackage{textcomp}
+\usepackage{amssymb}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}