--- a/src/HOL/Euclidean_Rings.thy Fri Sep 15 20:46:50 2023 +0100 +++ b/src/HOL/Euclidean_Rings.thy Sat Sep 16 06:38:44 2023 +0000 @@ -1651,7 +1651,6 @@ qed - subsection \<open>Division on \<^typ>\<open>int\<close>\<close> text \<open>