diff -r ee77d9d40be6 -r 6c369fec315a src/HOL/Library/Discrete.thy
--- a/src/HOL/Library/Discrete.thy	Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Library/Discrete.thy	Mon Jul 29 10:13:52 2024 +0100
@@ -63,7 +63,7 @@
   then show ?thesis by (simp add: log_rec)
 qed
 
-lemma log_exp [simp]: "log (2 ^ n) = n"
+lemma log_power [simp]: "log (2 ^ n) = n"
   by (induct n) simp_all
 
 lemma log_mono: "mono log"