hol.mm ql.mm demo0.mm miu.mm big-unifier.mm peano.mm have been added in PR
1722 https://github.com/metamath/set.mm/pull/1722
You or a volunteer can update these with the desired CC0 wording. (I won't
be doing that myself.)
Norm
On Monday, July 13, 2020 at 2:23:16 AM UTC-4, Giovanni Mascellani
Hi,
Il 12/07/20 21:42, Norman Megill ha scritto:
> While I expect all of the .mm's will be kept updated in the
> http://us.metamath.org/metamath/ directory indefinitely, I suggest we
> add the missing ones (hol.mm ql.mm demo0.mm miu.mm big-unifier.mm
> peano.mm) to the
On Sunday, July 12, 2020 at 1:12:32 PM UTC-4, Giovanni Mascellani wrote:
...
> I now want to include some example databases too, in a package called
> "metamath-databases". I see that set.mm, iset.mm and nf.mm are
> maintained in [1], which can be probably considered their canonical
>
