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
Thu, 02 Nov 2023 14:10:16 +0000
changeset 78882 c1bd24ca22b6
parent 78880 9ce8bf038444 (current diff)
parent 78881 fb6828831ef1 (diff)
child 78883 5de1c19ccd92
merged
--- a/src/HOL/Nat.thy	Thu Nov 02 14:31:01 2023 +0100
+++ b/src/HOL/Nat.thy	Thu Nov 02 14:10:16 2023 +0000
@@ -342,7 +342,10 @@
 lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
   by (simp add: diff_diff_add)
 
-lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
+lemma diff_Suc_1: "Suc n - 1 = n"
+  by simp
+
+lemma diff_Suc_1' [simp]: "Suc n - Suc 0 = n"
   by simp
isabelle