
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     Divisibility in monoids and rings
-  Author:    Clemens Ballarin, started 18 July 2008
+(*  Title:      Divisibility in monoids and rings
+    Author:     Clemens Ballarin, started 18 July 2008
 
 Based on work by Stephan Hohe.
 *)
@@ -156,6 +155,7 @@
       show "a \<in> Units G" by (simp add: Units_def, fast)
 qed
 
+
 subsection {* Divisibility and Association *}
 
 subsubsection {* Function definitions *}




