Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nat.thy
changeset 15281 bd4611956c7b
parent 15251 bb6f072c8d10
child 15341 254f6f00b60e 
--- a/src/HOL/Nat.thy	Fri Nov 12 20:55:04 2004 +0100
+++ b/src/HOL/Nat.thy	Sat Nov 13 07:47:34 2004 +0100
@@ -109,7 +109,7 @@
 
 text {* Injectiveness of @{term Suc} *}
 
-lemma inj_Suc: "inj Suc"
+lemma inj_Suc: "inj_on Suc N"
   apply (unfold Suc_def)
   apply (rule inj_onI)
   apply (drule inj_on_Abs_Nat [THEN inj_onD])
isabelle