diff -r 465846b611d5 -r 7181130f5872 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Jun 23 17:43:31 2021 +0000
+++ b/src/HOL/Power.thy	Wed Jun 23 17:43:31 2021 +0000
@@ -908,7 +908,7 @@
 lemma power_gt_expt: "n > Suc 0 \<Longrightarrow> n^k > k"
   by (induction k) (auto simp: less_trans_Suc n_less_m_mult_n)
 
-lemma less_exp:
+lemma less_exp [simp]:
   \<open>n < 2 ^ n\<close>
   by (simp add: power_gt_expt)