credits to Paulo and Martin
authorpaulson <lp15@cam.ac.uk>
Sat, 30 Jun 2018 18:58:13 +0100
changeset 68552 391e89e03eef
parent 68551 b680e74eb6f2
child 68553 22d51874f37d
child 68555 5273df52ad83
child 68558 5a836f1b588c
credits to Paulo and Martin
src/HOL/Algebra/Module.thy
src/HOL/Algebra/Ring.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
--- 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