Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorpaulson
Mon, 03 Feb 2025 18:22:33 +0000
changeset 82061 87f65613122d
parent 82059 133b41bce661 (current diff)
parent 82060 9adc1ef1e8dc (diff)
child 82073 879be333e939
merged
--- a/src/HOL/Nat.thy	Mon Feb 03 13:17:37 2025 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 03 18:22:33 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
isabelle