# HG changeset patch
# User wenzelm
# Date 1429106278 -7200
# Node ID 019347f8dc88b532d5ed64d2b3d48f15576d3acd
# Parent  55cb9462e602bae33ec6db23c6ffdb87f91136f8
use wasysym for \<hole>;

diff -r 55cb9462e602 -r 019347f8dc88 src/HOL/Library/document/root.tex
--- a/src/HOL/Library/document/root.tex	Wed Apr 15 15:27:45 2015 +0200
+++ b/src/HOL/Library/document/root.tex	Wed Apr 15 15:57:58 2015 +0200
@@ -2,7 +2,7 @@
 \usepackage{ifthen}
 \usepackage[utf8]{inputenc}
 \usepackage[english]{babel}
-\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp}
+\usepackage{isabelle,isabellesym,amssymb,stmaryrd,textcomp,wasysym}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}
diff -r 55cb9462e602 -r 019347f8dc88 src/HOL/ex/document/root.tex
--- a/src/HOL/ex/document/root.tex	Wed Apr 15 15:27:45 2015 +0200
+++ b/src/HOL/ex/document/root.tex	Wed Apr 15 15:57:58 2015 +0200
@@ -4,6 +4,7 @@
 \usepackage[english]{babel}
 \usepackage{textcomp}
 \usepackage{amssymb}
+\usepackage{wasysym}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}