src/HOL/Library/Discrete_Functions.thy

--- a/src/HOL/Library/Discrete_Functions.thy	Sat May 24 09:06:26 2025 +0200
+++ b/src/HOL/Library/Discrete_Functions.thy	Wed May 28 17:49:22 2025 +0200
@@ -200,8 +200,10 @@
 
 lemma floor_sqrt_code[code]: "floor_sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})"
 proof -
-  from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> n}" by auto
-  then show ?thesis by (simp add: floor_sqrt_def Set.filter_def)
+  from power2_nat_le_imp_le [of _ n]
+    have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> n}" by auto
+    then show ?thesis
+    by (simp add: floor_sqrt_def)
 qed
 
 lemma floor_sqrt_inverse_power2 [simp]: "floor_sqrt (n\<^sup>2) = n"