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"