# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530573316 -3600
# Node ID a3723b11bd60390b9948e1586104cda57c6fdbee
# Parent  6dff90eba4931f85856ff71fe8e7957a348cd63d
more latex problems

diff -r 6dff90eba493 -r a3723b11bd60 src/HOL/Algebra/Ring_Divisibility.thy
--- 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>"
diff -r 6dff90eba493 -r a3723b11bd60 src/HOL/Algebra/document/root.tex
--- 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