
diff -r 4ec8e654112f -r 2865a6618cba src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Library/Float.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -1774,7 +1774,7 @@
     by transfer (simp add: plus_down_def ac_simps Let_def)
 qed
 
-lemma compute_float_plus_down_naive[code]: "float_plus_down p x y = float_round_down p (x + y)"
+lemma compute_float_plus_down_naive: "float_plus_down p x y = float_round_down p (x + y)"
   by transfer (auto simp: plus_down_def)
 
 qualified lemma compute_float_plus_down[code]:




