# HG changeset patch
# User blanchet
# Date 1391446550 -3600
# Node ID 3951ced4156cad9c729d0cb80038aac626fea1c9
# Parent  30d874dc70008e0004cb5ca8332fb2c8e4f0174c
searchable underscores

diff -r 30d874dc7000 -r 3951ced4156c src/Doc/Datatypes/Datatypes.thy
--- 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
diff -r 30d874dc7000 -r 3951ced4156c src/Doc/Datatypes/document/root.tex
--- 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
diff -r 30d874dc7000 -r 3951ced4156c src/Doc/Nitpick/document/root.tex
--- 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.
diff -r 30d874dc7000 -r 3951ced4156c src/Doc/Sledgehammer/document/root.tex
--- 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