# HG changeset patch
# User haftmann
# Date 1710355181 0
# Node ID b187c1b9d6a9353901d3c49ed58ebacc6b16d609
# Parent  7b4b524cdee27cf96909359233584704b8d570b6
Tuned proofs

diff -r 7b4b524cdee2 -r b187c1b9d6a9 src/HOL/Algebra/Polynomial_Divisibility.thy
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy	Wed Mar 13 23:27:44 2024 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy	Wed Mar 13 18:39:41 2024 +0000
@@ -2082,7 +2082,7 @@
     using univ_poly_is_principal[OF assms(1)] .
 
   show ?thesis
-  proof (intro no_atp(10)[OF subsetI subsetI])
+  proof (rule order_antisym; rule subsetI)
     fix q assume "q \<in> { q \<in> carrier (K[X]). length q \<le> degree p }"
     then have "q \<in> carrier (K[X])" and "length q \<le> degree p"
       by simp+
@@ -2125,7 +2125,7 @@
     using univ_poly_is_domain[OF subring] .
 
   show ?thesis
-  proof (intro no_atp(10)[OF subsetI subsetI])
+  proof (rule order_antisym; rule subsetI)
     fix q assume "q \<in> { q \<in> carrier (K[X]). length q \<le> n }"
     then have q: "q \<in> carrier (K[X])" "length q \<le> n"
       by simp+