# HG changeset patch # User wenzelm # Date 1429106278 -7200 # Node ID 019347f8dc88b532d5ed64d2b3d48f15576d3acd # Parent 55cb9462e602bae33ec6db23c6ffdb87f91136f8 use wasysym for \; 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}