# HG changeset patch
# User blanchet
# Date 1459609887 -7200
# Node ID 19387866eace3e65bceeeda1eece3ba2ac60e0e8
# Parent  d0fc75798bafc38b866f14cb40dab6adf71f33d5
tuned LaTeX

diff -r d0fc75798baf -r 19387866eace src/Doc/Corec/Corec.thy
--- a/src/Doc/Corec/Corec.thy	Sat Apr 02 17:02:37 2016 +0200
+++ b/src/Doc/Corec/Corec.thy	Sat Apr 02 17:11:27 2016 +0200
@@ -812,11 +812,11 @@
 
 \item[@{text "f."}\hthm{cong_trans}]
 
-\item[@{text "f."}\hthm{cong_C\textsubscript{1}}, \ldots, @{text "f."}\hthm{cong_C\textsubscript{\textit{n}}}] ~ \\
+\item[@{text "f."}\hthm{cong_C}@{text "\<^sub>1"}, \ldots, @{text "f."}\hthm{cong_C}@{text "\<^sub>n"}] ~ \\
 where @{text "C\<^sub>1"}, @{text "\<dots>"}, @{text "C\<^sub>n"} are @{text t}'s
 constructors
 
-\item[@{text "f."}\hthm{cong_f\textsubscript{1}}, \ldots, @{text "f."}\hthm{cong_f\textsubscript{\textit{m}}}] ~ \\
+\item[@{text "f."}\hthm{cong_f}@{text "\<^sub>1"}, \ldots, @{text "f."}\hthm{cong_f}@{text "\<^sub>m"}] ~ \\
 where @{text "f\<^sub>1"}, @{text "\<dots>"}, @{text "f\<^sub>m"} are the available
 friends for @{text t}
 
diff -r d0fc75798baf -r 19387866eace src/Doc/Corec/document/root.tex
--- a/src/Doc/Corec/document/root.tex	Sat Apr 02 17:02:37 2016 +0200
+++ b/src/Doc/Corec/document/root.tex	Sat Apr 02 17:11:27 2016 +0200
@@ -18,7 +18,6 @@
 \usepackage{railsetup}
 \usepackage{framed}
 \usepackage{regexpatch}
-\usepackage{subscript}
 
 \makeatletter
 \xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}%
diff -r d0fc75798baf -r 19387866eace src/Doc/Datatypes/document/root.tex
--- a/src/Doc/Datatypes/document/root.tex	Sat Apr 02 17:02:37 2016 +0200
+++ b/src/Doc/Datatypes/document/root.tex	Sat Apr 02 17:11:27 2016 +0200
@@ -18,7 +18,6 @@
 \usepackage{railsetup}
 \usepackage{framed}
 \usepackage{regexpatch}
-\usepackage{subscript}
 
 \makeatletter
 \xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}%