--- a/src/HOL/Algebra/AbelCoset.thy Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Sun Mar 21 17:12:31 2010 +0100
@@ -1,13 +1,11 @@
-(*
- Title: HOL/Algebra/AbelCoset.thy
- Author: Stephan Hohe, TU Muenchen
+(* Title: HOL/Algebra/AbelCoset.thy
+ Author: Stephan Hohe, TU Muenchen
*)
theory AbelCoset
imports Coset Ring
begin
-
subsection {* More Lifting from Groups to Abelian Groups *}
subsubsection {* Definitions *}
@@ -520,6 +518,7 @@
text {* The isomorphism theorems have been omitted from lifting, at
least for now *}
+
subsubsection{*The First Isomorphism Theorem*}
text{*The quotient by the kernel of a homomorphism is isomorphic to the
@@ -642,6 +641,7 @@
by (rule group_hom.FactGroup_iso[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+
subsubsection {* Cosets *}
text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
@@ -726,7 +726,6 @@
folded A_RCOSETS_def, simplified monoid_record_simps])
-
subsubsection {* Addition of Subgroups *}
lemma (in abelian_monoid) set_add_closed: