--- a/src/HOL/Algebra/Ring_Divisibility.thy Mon Jul 02 23:06:34 2018 +0100
+++ b/src/HOL/Algebra/Ring_Divisibility.thy Tue Jul 03 00:15:16 2018 +0100
@@ -8,7 +8,7 @@
begin
-section \<open>Definitions ported from Multiplicative_Group.thy\<close>
+section \<open>Definitions ported from @{text "Multiplicative_Group.thy"}\<close>
definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
"mult_of R \<equiv> \<lparr> carrier = carrier R - { \<zero>\<^bsub>R\<^esub> }, mult = mult R, one = \<one>\<^bsub>R\<^esub> \<rparr>"
--- a/src/HOL/Algebra/document/root.tex Mon Jul 02 23:06:34 2018 +0100
+++ b/src/HOL/Algebra/document/root.tex Tue Jul 03 00:15:16 2018 +0100
@@ -5,7 +5,7 @@
\usepackage{textcomp}
\usepackage[utf8]{inputenc}
\usepackage[only,bigsqcap]{stmaryrd}
-%\usepackage{amsmath}
+\usepackage{amsmath}
% this should be the last package used
\usepackage{pdfsetup}
@@ -18,7 +18,7 @@
\title{The Isabelle/HOL Algebra Library}
\author{Clemens Ballarin (Editor)}
-\date{With contributions by Jesús Aransay, Clemens Ballarin, Stephan Hohe,
+\date{With contributions by Jesús Aransay, Clemens Ballarin, Martin Baillon, Paulo Emílio de Vilhena, Stephan Hohe,
Florian Kammüller and Lawrence C Paulson \\
\today}
\maketitle