# HG changeset patch
# User Manuel Eberl <manuel@pruvisto.org>
# Date 1634314174 -7200
# Node ID d592354c4a26eca1233574925452224675781602
# Parent  2ff001a8c9f22f0def7b15c441dd6ea75098f0a5
removed some 'private' modifiers from HOL-Computational_Algebra

diff -r 2ff001a8c9f2 -r d592354c4a26 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Oct 18 18:33:46 2021 +0200
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Oct 15 18:09:34 2021 +0200
@@ -313,7 +313,7 @@
 context
 begin
 
-private lemma prime_elem_powerD:
+lemma prime_elem_powerD:
   assumes "prime_elem (p ^ n)"
   shows   "prime_elem p \<and> n = 1"
 proof (cases n)
diff -r 2ff001a8c9f2 -r d592354c4a26 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Oct 18 18:33:46 2021 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Fri Oct 15 18:09:34 2021 +0200
@@ -525,7 +525,7 @@
   qed
 qed
 
-private lemma irreducible_imp_prime_poly:
+lemma irreducible_imp_prime_poly:
   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
   assumes "irreducible p"
   shows   "prime_elem p"
@@ -615,7 +615,7 @@
  
 subsection \<open>Prime factorisation of polynomials\<close>   
 
-private lemma poly_prime_factorization_exists_content_1:
+lemma poly_prime_factorization_exists_content_1:
   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
   assumes "p \<noteq> 0" "content p = 1"
   shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"