Jon P wrote: >> Quick question: Why are the following sections marked as depricated in >> set.mm? ... >> PART 18 ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS >(DEPRECATED) >> >> PART 19 COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)
Norman Megill: >The intent is for these deprecated sections to be deleted at some point in >the future, once their theorems have extensible structure versions... >> PART 20 COMPLEX HILBERT SPACE EXPLORER (DEPRECATED) >The "Hilbert Space Explorer" section is deprecated because it starts >from >the axioms (not just definitions) for a single Hilbert space added to >ZFC. I intend to create a small pull request (a few lines in total) to document that information in those set.mm headers. That way future readers will know why it's there, and maybe even be encouraged to help. --- 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/C31860CA-4226-4CA8-83FC-FC25D87EA963%40dwheeler.com.
