--- a/src/HOL/Algebra/Sylow.thy Thu Aug 03 14:53:57 2006 +0200
+++ b/src/HOL/Algebra/Sylow.thy Thu Aug 03 14:57:26 2006 +0200
@@ -3,9 +3,10 @@
Author: Florian Kammueller, with new proofs by L C Paulson
*)
-header {* Sylow's theorem *}
+theory Sylow imports Coset begin
-theory Sylow imports Coset begin
+
+section {* Sylow's Theorem *}
text {*
See also \cite{Kammueller-Paulson:1999}.
@@ -50,9 +51,9 @@
apply (blast elim!: quotientE)
done
+
subsection{*Main Part of the Proof*}
-
locale sylow_central = sylow +
fixes H and M1 and M
assumes M_in_quot: "M \<in> calM // RelM"
@@ -265,7 +266,7 @@
done
-subsubsection{*The opposite injection*}
+subsubsection{*The Opposite Injection*}
lemma (in sylow_central) H_elem_map:
"H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
@@ -362,6 +363,9 @@
lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
by (simp add: sylow_def group_def)
+
+subsection {* Sylow's Theorem *}
+
theorem sylow_thm:
"[| prime p; group(G); order(G) = (p^a) * m; finite (carrier G)|]
==> \<exists>H. subgroup H G & card(H) = p^a"