credits to Paulo and Martin
authorpaulson <lp15@cam.ac.uk>
Sat Jun 30 18:58:13 2018 +0100 (9 months ago)
changeset 68552391e89e03eef
parent 68551 b680e74eb6f2
child 68554 5273df52ad83
child 68555 22d51874f37d
child 68557 5a836f1b588c
credits to Paulo and Martin
src/HOL/Algebra/Module.thy
src/HOL/Algebra/Ring.thy
     1.1 --- a/src/HOL/Algebra/Module.thy	Sat Jun 30 15:44:04 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Module.thy	Sat Jun 30 18:58:13 2018 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Algebra/Module.thy
     1.5      Author:     Clemens Ballarin, started 15 April 2003
     1.6 -    Copyright:  Clemens Ballarin
     1.7 +		with contributions by Martin Baillon
     1.8  *)
     1.9  
    1.10  theory Module
     2.1 --- a/src/HOL/Algebra/Ring.thy	Sat Jun 30 15:44:04 2018 +0100
     2.2 +++ b/src/HOL/Algebra/Ring.thy	Sat Jun 30 18:58:13 2018 +0100
     2.3 @@ -1,6 +1,7 @@
     2.4  (*  Title:      HOL/Algebra/Ring.thy
     2.5      Author:     Clemens Ballarin, started 9 December 1996
     2.6 -    Copyright:  Clemens Ballarin
     2.7 +
     2.8 +With contributions by Martin Baillon
     2.9  *)
    2.10  
    2.11  theory Ring