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)
```