# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530381493 -3600
# Node ID 391e89e03eef99743610d82b7e88051ac58e974e
# Parent  b680e74eb6f2699c312d1dbe19c08c56681f5dd2
credits to Paulo and Martin

diff -r b680e74eb6f2 -r 391e89e03eef src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Sat Jun 30 15:44:04 2018 +0100
+++ b/src/HOL/Algebra/Module.thy	Sat Jun 30 18:58:13 2018 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Algebra/Module.thy
     Author:     Clemens Ballarin, started 15 April 2003
-    Copyright:  Clemens Ballarin
+		with contributions by Martin Baillon
 *)
 
 theory Module
diff -r b680e74eb6f2 -r 391e89e03eef src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sat Jun 30 15:44:04 2018 +0100
+++ b/src/HOL/Algebra/Ring.thy	Sat Jun 30 18:58:13 2018 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Algebra/Ring.thy
     Author:     Clemens Ballarin, started 9 December 1996
-    Copyright:  Clemens Ballarin
+
+With contributions by Martin Baillon
 *)
 
 theory Ring