--- a/src/Doc/Datatypes/Datatypes.thy Mon Feb 03 17:18:38 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Feb 03 17:55:50 2014 +0100
@@ -1103,7 +1103,7 @@
Pattern matching is only available for the argument on which the recursion takes
place. Fortunately, it is easy to generate pattern-maching equations using the
\keyw{simps\_of\_case} command provided by the theory
-\verb|~~/src/HOL/Library/Simps_Case_Conv|.
+\verb|~~/src/HOL/|\allowbreak\verb|Library/|\allowbreak\verb|Simps_Case_Conv|.
*}
simps_of_case at_simps: at.simps
--- a/src/Doc/Datatypes/document/root.tex Mon Feb 03 17:18:38 2014 +0100
+++ b/src/Doc/Datatypes/document/root.tex Mon Feb 03 17:55:50 2014 +0100
@@ -1,4 +1,5 @@
\documentclass[12pt,a4paper]{article} % fleqn
+\usepackage[T1]{fontenc}
\usepackage{cite}
\usepackage{enumitem}
\usepackage{footmisc}
@@ -17,6 +18,8 @@
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
\newbox\boxA
\setbox\boxA=\hbox{\ }
\parindent=4\wd\boxA
@@ -52,6 +55,9 @@
Dmitriy Traytel \\
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
\hbox{}}
+
+\urlstyle{tt}
+
\begin{document}
\maketitle
--- a/src/Doc/Nitpick/document/root.tex Mon Feb 03 17:18:38 2014 +0100
+++ b/src/Doc/Nitpick/document/root.tex Mon Feb 03 17:55:50 2014 +0100
@@ -40,6 +40,8 @@
\urlstyle{tt}
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
\begin{document}
%%% TYPESETTING
@@ -127,7 +129,7 @@
To run Nitpick, you must also make sure that the theory \textit{Nitpick} is
imported---this is rarely a problem in practice since it is part of
\textit{Main}. The examples presented in this manual can be found
-in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory.
+in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory.
The known bugs and limitations at the time of writing are listed in
\S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either
the tool or the manual should be directed to the author at \authoremail.
--- a/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 17:18:38 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Feb 03 17:55:50 2014 +0100
@@ -42,6 +42,8 @@
\urlstyle{tt}
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
\begin{document}
%%% TYPESETTING