--- a/src/HOL/Algebra/Ideal.thy Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Ideal.thy Sun Mar 21 17:12:31 2010 +0100
@@ -1,6 +1,5 @@
-(*
- Title: HOL/Algebra/CIdeal.thy
- Author: Stephan Hohe, TU Muenchen
+(* Title: HOL/Algebra/CIdeal.thy
+ Author: Stephan Hohe, TU Muenchen
*)
theory Ideal
@@ -45,6 +44,7 @@
done
qed
+
subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
definition
@@ -71,6 +71,7 @@
show ?thesis by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
qed
+
subsubsection {* Maximal Ideals *}
locale maximalideal = ideal +
@@ -93,6 +94,7 @@
(rule is_ideal, rule I_notcarr, rule I_maximal)
qed
+
subsubsection {* Prime Ideals *}
locale primeideal = ideal + cring +
@@ -139,6 +141,7 @@
done
qed
+
subsection {* Special Ideals *}
lemma (in ring) zeroideal:
@@ -867,6 +870,7 @@
qed
qed
+
subsection {* Derived Theorems *}
--"A non-zero cring that has only the two trivial ideals is a field"