Have you looked into WRITE SOURCE set.mm/SPLIT ? That might be exactly what you are looking for in terms of propositional and predicate logic, and maybe a good start for set theory (in which the axioms are spread out over a larger section of the file).
On September 11, 2019 1:30:42 PM PDT, Ishan Murphy <[email protected]> wrote: >I'd like to use the set theory portion of set.mm as a starting point >for >another theorem database. However, set.mm is several megabytes large, >and I >don't need most of it. Has anyone made a condensed version of it that >only >includes the "essential" parts of propositional logic and set theory, >or >should I just copy the axioms and pick out the theorems I need? > >-- >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/31c9eb86-1994-4d3e-ab71-4e0767de3a74%40googlegroups.com. -- 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/E6690107-FA12-4897-9A3C-2F05E39B9850%40panix.com.
