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