# HG changeset patch
# User wenzelm
# Date 1139772779 -3600
# Node ID 80eb6640f3d57d4e7163a8a2c29754d1612cdda6
# Parent  5652a536b7e8f2c78e617208b5f8c57b5250c360
\usepackage{amssymb};

diff -r 5652a536b7e8 -r 80eb6640f3d5 src/HOL/ex/document/root.tex
--- 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}