diff -r e86a7b8d7ada -r 9adc1ef1e8dc src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Jan 26 13:27:41 2025 +0000
+++ b/src/HOL/Nat.thy	Mon Feb 03 18:22:25 2025 +0000
@@ -1296,6 +1296,8 @@
   for a b :: nat
   \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
   by (auto split: nat_diff_split)
+  
+lemmas nat_diff_splits = nat_diff_split nat_diff_split_asm
 
 lemma Suc_pred': "0 < n \<Longrightarrow> n = Suc(n - 1)"
   by simp