src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Nat.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -215,7 +215,7 @@
 
 primrec plus_nat
   where
-    add_0: "0 + n = (n::nat)"
+    add_0 [code]: "0 + n = (n::nat)"
   | add_Suc: "Suc m + n = Suc (m + n)"
 
 lemma add_0_right [simp]: "m + 0 = m"
@@ -225,8 +225,6 @@
 lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
   by (induct m) simp_all
 
-declare add_0 [code]
-
 lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
   by simp
 
@@ -1501,8 +1499,8 @@
   where funpow_code_def [code_abbrev]: "funpow = compow"
 
 lemma [code]:
+  "funpow 0 f = id"
   "funpow (Suc n) f = f \<circ> funpow n f"
-  "funpow 0 f = id"
   by (simp_all add: funpow_code_def)
 
 end