# HG changeset patch
# User blanchet
# Date 1391730484 -3600
# Node ID b5b64d9d1002f8b8f6577a9f5b6dbfd972d63ff5
# Parent  6ca9df01ac8c875e22320c7fdb4fd91bb1f87d27
more docs

diff -r 6ca9df01ac8c -r b5b64d9d1002 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Feb 07 00:19:02 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Feb 07 00:48:04 2014 +0100
@@ -1847,8 +1847,12 @@
 text {*
 This generates the lemma collection @{thm [source] lappend_simps}:
 %
-\[@{thm lappend_simps(1)[no_vars]}
-  \qquad @{thm lappend_simps(2)[no_vars]}\]
+\begin{gather*%
+}
+  @{thm lappend_simps(1)[no_vars]} \\
+  @{thm lappend_simps(2)[no_vars]}
+\end{gather*%
+}
 %
 Corecursion is useful to specify not only functions but also infinite objects:
 *}
diff -r 6ca9df01ac8c -r b5b64d9d1002 src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Fri Feb 07 00:19:02 2014 +0100
+++ b/src/Doc/Datatypes/document/root.tex	Fri Feb 07 00:48:04 2014 +0100
@@ -1,5 +1,6 @@
 \documentclass[12pt,a4paper]{article} % fleqn
 \usepackage[T1]{fontenc}
+\usepackage{amsmath}
 \usepackage{cite}
 \usepackage{enumitem}
 \usepackage{footmisc}
@@ -33,14 +34,16 @@
 \newcommand{\hthm}[1]{\textbf{\textit{#1}}}
 
 %\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
-\renewcommand{\isactrlsub}[1]{\/$\sb{#1}$}
-\renewcommand{\isadigit}[1]{\/\ensuremath{\mathrm{#1}}}
-\renewcommand{\isacharprime}{\isamath{{'}\mskip-2mu}}
-\renewcommand{\isacharunderscore}{\mbox{\_}}
-\renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
-\renewcommand{\isachardoublequote}{\mbox{\upshape{``}}}
-\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\kern.1ex}}
-\renewcommand{\isachardoublequoteclose}{\/\kern.15ex\mbox{\upshape{''}}}
+\renewcommand\isactrlsub[1]{\/$\sb{#1}$}
+\renewcommand\isadigit[1]{\/\ensuremath{\mathrm{#1}}}
+\renewcommand\isacharprime{\isamath{{'}\mskip-2mu}}
+\renewcommand\isacharunderscore{\mbox{\_}}
+\renewcommand\isacharunderscorekeyword{\mbox{\_}}
+\renewcommand\isachardoublequote{\mbox{\upshape{``}}}
+\renewcommand\isachardoublequoteopen{\mbox{\upshape{``}\kern.1ex}}
+\renewcommand\isachardoublequoteclose{\/\kern.15ex\mbox{\upshape{''}}}
+\renewcommand\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\renewcommand\isacharverbatimclose{\isacharasterisk\isacharbraceright}
 
 \hyphenation{isa-belle}
 
@@ -53,7 +56,7 @@
 Lorenz Panny, \\
 Andrei Popescu, and
 Dmitriy Traytel \\
-{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
+{\normalsize Fakult\"at f\"ur Informatik, Technische Universit\"at M\"unchen} \\
 \hbox{}}
 
 \urlstyle{tt}