--- 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