src/HOL/Algebra/IntRing.thy
 changeset 27717 21bbd410ba04 parent 27713 95b36bfe7fc4 child 28085 914183e229e9
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Aug 01 17:41:37 2008 +0200
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Aug 01 18:10:52 2008 +0200
1.3 @@ -5,7 +5,7 @@
1.4  *)
1.5
1.6  theory IntRing
1.7 -imports QuotRing Int
1.8 +imports QuotRing Int Primes
1.9  begin
1.10
1.11
1.12 @@ -62,10 +62,7 @@
1.13  done
1.14
1.15
1.16 -
1.17 -subsection {* The Set of Integers as Algebraic Structure *}
1.18 -
1.19 -subsubsection {* Definition of @{text "\<Z>"} *}
1.20 +subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
1.21
1.22  constdefs
1.23    int_ring :: "int ring" ("\<Z>")
1.24 @@ -94,7 +91,7 @@
1.25   apply (unfold int_ring_def, simp+)
1.26  done
1.27  *)
1.28 -subsubsection {* Interpretations *}
1.29 +subsection {* Interpretations *}
1.30
1.31  text {* Since definitions of derived operations are global, their
1.32    interpretation needs to be done as early as possible --- that is,
1.33 @@ -254,7 +251,7 @@
1.34    by unfold_locales clarsimp
1.35
1.36
1.37 -subsubsection {* Generated Ideals of @{text "\<Z>"} *}
1.38 +subsection {* Generated Ideals of @{text "\<Z>"} *}
1.39
1.40  lemma int_Idl:
1.41    "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
1.42 @@ -342,7 +339,7 @@
1.43  qed
1.44
1.45
1.46 -subsubsection {* Ideals and Divisibility *}
1.47 +subsection {* Ideals and Divisibility *}
1.48
1.49  lemma int_Idl_subset_ideal:
1.50    "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
1.51 @@ -376,7 +373,7 @@
1.52  done
1.53
1.54
1.55 -subsubsection {* Ideals and the Modulus *}
1.56 +subsection {* Ideals and the Modulus *}
1.57
1.58  constdefs
1.59     ZMod :: "int => int => int set"
1.60 @@ -459,7 +456,7 @@
1.61  by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
1.62
1.63
1.64 -subsubsection {* Factorization *}
1.65 +subsection {* Factorization *}
1.66
1.67  constdefs
1.68    ZFact :: "int \<Rightarrow> int set ring"
```