src/HOL/Algebra/IntRing.thy
changeset 68399 0b71d08528f0
parent 67443 3abf6a722518
child 68561 5e85cda58af6
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Jun 05 16:35:52 2018 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Jun 06 14:25:53 2018 +0100
     1.3 @@ -4,7 +4,7 @@
     1.4  *)
     1.5  
     1.6  theory IntRing
     1.7 -imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
     1.8 +imports "HOL-Computational_Algebra.Primes" QuotRing Lattice 
     1.9  begin
    1.10  
    1.11  section \<open>The Ring of Integers\<close>
    1.12 @@ -229,7 +229,7 @@
    1.13    by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
    1.14  
    1.15  lemma prime_primeideal:
    1.16 -  assumes prime: "prime p"
    1.17 +  assumes prime: "Factorial_Ring.prime p"
    1.18    shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
    1.19  apply (rule primeidealI)
    1.20     apply (rule int.genideal_ideal, simp)
    1.21 @@ -404,7 +404,7 @@
    1.22    done
    1.23  
    1.24  lemma ZFact_prime_is_domain:
    1.25 -  assumes pprime: "prime p"
    1.26 +  assumes pprime: "Factorial_Ring.prime p"
    1.27    shows "domain (ZFact p)"
    1.28    apply (unfold ZFact_def)
    1.29    apply (rule primeideal.quotient_is_domain)