Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Float.thy
changeset 82774 2865a6618cba
parent 81806 602639414559 
--- 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]:
isabelle