--- a/src/HOL/Algebra/Divisibility.thy Sun Mar 13 22:24:10 2011 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Sun Mar 13 22:55:50 2011 +0100
@@ -1,9 +1,10 @@
-(* Title: Divisibility in monoids and rings
- Author: Clemens Ballarin, started 18 July 2008
-
-Based on work by Stephan Hohe.
+(* Title: HOL/Algebra/Divisibility.thy
+ Author: Clemens Ballarin
+ Author: Stephan Hohe
*)
+header {* Divisibility in monoids and rings *}
+
theory Divisibility
imports "~~/src/HOL/Library/Permutation" Coset Group
begin