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.
fixed the simplification of Suc n - 1
authorpaulson <lp15@cam.ac.uk>
Thu, 02 Nov 2023 14:10:08 +0000
changeset 78881 fb6828831ef1
parent 78872 711acefe97a3
child 78882 c1bd24ca22b6
fixed the simplification of Suc n - 1
src/HOL/Nat.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nat.thy	Tue Oct 31 17:32:56 2023 +0100
+++ b/src/HOL/Nat.thy	Thu Nov 02 14:10:08 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