For what it's worth, here's some git history:
$ git log -L '/nnne0ALT \$p/,+1:set.mm'
commit df12e3e7168f44afd3771b5aba5286a66f1ae8f6
Author: Steven Nguyen <[email protected]>
Date: Tue Jan 31 14:18:36 2023 -0600
rename equsb3lem et al to equsb3v et al, rmv ax-mulgt0 from 0nnn (#3018)
* rename equsb3lem et al to equsb3v et al, rmv ax-mulgt0 from nnnn0
also reduces ax-13 from the renamed elsb3v and elsb4v
I wonder how many of these improvements to set.mm transfer to iset.mm
* rewrap
* rmv elsb3vOLD + elsb4vOLD
tag drift
diff --git a/set.mm b/set.mm
--- a/set.mm
+++ b/set.mm
@@ -121870,2 +121896,1 @@
- $( A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) $)
- nnne0 $p |- ( A e. NN -> A =/= 0 ) $=
+ nnne0ALT $p |- ( A e. NN -> A =/= 0 ) $=
commit 98e1d43acb1e96b6ca2010bd83fa2894032074ee
Author: nmegill <[email protected]>
Date: Mon Oct 15 19:55:51 2018 -0400
set.mm - change 'natural number' to 'positive integer' in NN comments
diff --git a/set.mm b/set.mm
--- a/set.mm
+++ b/set.mm
@@ -119172,2 +119173,2 @@
- $( A natural number is nonzero. (Contributed by NM, 27-Sep-1999.) $)
+ $( A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) $)
nnne0 $p |- ( A e. NN -> A =/= 0 ) $=
commit c5fe509062dcca53a4d0572a71c953d5bd27d4a1
Author: Norm <[email protected]>
Date: Thu Nov 5 13:08:37 2015 -0500
Handed to Mario to identify missing contributors
diff --git a/set.mm b/set.mm
--- a/set.mm
+++ b/set.mm
@@ -112270,2 +116100,2 @@
- $( A natural number is nonzero. $)
+ $( A natural number is nonzero. (Contributed by NM, 27-Sep-1999.) $)
nnne0 $p |- ( A e. NN -> A =/= 0 ) $=
commit 0d2cf5049823b116baad01ff6be6481219113d8e
Author: Norm <[email protected]>
Date: Tue May 12 09:14:21 2015 -0400
stable release, archive name set.mm.2011-06-27
diff --git a/set.mm b/set.mm
--- a/set.mm
+++ b/set.mm
@@ -69477,2 +71839,2 @@
- $( A natural number is non-zero. $)
+ $( A natural number is nonzero. $)
nnne0 $p |- ( A e. NN -> A =/= 0 ) $=
commit 45f6474f112a5cf2d76cd1aaf659be990bff61c5
Author: Norm <[email protected]>
Date: Tue May 12 09:14:16 2015 -0400
stable release, archive name set.mm.2010-08-29
diff --git a/set.mm b/set.mm
--- a/set.mm
+++ b/set.mm
@@ -67129,0 +69477,2 @@
+ $( A natural number is non-zero. $)
+ nnne0 $p |- ( A e. NN -> A =/= 0 ) $=
Mario Carneiro <[email protected]> wrote:
> It sounds like we were unable to prevent a proof modification in this case.
> We'll have to go back through the history to find out what the original
> proof was and how it degenerated.
>
> On Wed, Feb 1, 2023 at 12:54 PM Zheng Fan <[email protected]> wrote:
>
> > The proof of nnne0ALT is a thin wrapper of 0nnn, which is in turn a thin
> > wrapper of nnne0, which makes me think why this alternative proof is kept.
> > The caption says that it is supposed to be a shorter proof using more
> > axioms, but it seems not the case, at least for the current version of
> > set.mm.
> >
> > --
> > You received this message because you are subscribed to the Google Groups
> > "Metamath" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to [email protected].
> > To view this discussion on the web visit
> > https://groups.google.com/d/msgid/metamath/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com
> > <https://groups.google.com/d/msgid/metamath/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com?utm_medium=email&utm_source=footer>
> > .
> >
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/27NLFZVAI8UXL.2TW1AWPTTYMOB%40wilsonb.com.
