> On Jul 3, 2023, at 10:58 PM, Marshall Stoner <[email protected]> wrote:
>
> Thanks. I was not very specific because I was waiting to make sure I was
> actually subscribed to the group. I attached the pdf to show you the idea of
> what I'm doing. I would like to provide the quickest and easiest way forward
> to that start of ZFC theory while still being formally precise. Like you
> said, there are far too many theorems to easily convert into a "book form"
> that includes everything.
It's up to you, but one possibility would be create a document in the set.mm
repo
with the name `mmSOMETHING.raw.html`. These are just normal HTML files, but
anything in
`...` is processed by metamath-exe to generate nicer-looking HTML for the
equations.
This is how we generate, for example, mmcomplex.raw.html - this is processed and
turned into mmcomplex.html for use as a final document. There's no obligation
to use
that mechanism, but you might find it useful.
I've thought about creating a "tour guide" of sorts that points out and
explains the highlights
(without going into the details of *every* theorem) - it sounds like you might
have a somewhat
similar goal. If it's in the set.mm repo, it can be updated along with the rest
of set.mm.
--- David A. Wheeler
--
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/A659D0DC-5DB5-4D10-B7D9-CFB0660EE959%40dwheeler.com.
