I think the header is centered the same as say mmzfcnd.raw.html but the lack of the metamath logo causes a distortion in the space available in which to center the title. The HTML validation was fixed by updating the IMG tags to have ALT descriptions and be more HTML-like. There were some broken table header closing tags, now fixed. The main content table has had its maximum width capped at 90% so that you can see it is centered as well, and the column widths have been adjusted to prevent runaway width allocation in the event of a very wide display.
The English still needs work as I see at least two commas that have no justification for their existence and I haven't yet tackled the really hard to format Frege notations introduced starting with 69. But the work in progress has been shared on my new fregepack branch https://github.com/arpie-steele/set.mm/tree/fregepack On Monday, November 2, 2020 at 12:05:04 PM UTC-8 Norman Megill wrote: > This seems very useful for understanding the Frege notation. I can add it > to the mpeuni directory. However, the mmfrege.html file should pass > http://validator.w3.org, and the main header should be centered like on > the other website pages. Also, there are a large number of separate svg > files; perhaps you can prefix the svg file names with "_frege_" so they can > be more easily identified. Currently we are keeping svg files in the same > directory as html files (perhaps not the greatest practice, but it's what > the site creation scripts currently expect), so the you would reference > "fregenotation/jABinS.svg" as "_frege_jABinS.svg" in the html file. > > For referencing mmfrege.html in a set.mm comment, you can use "~ > mmfrege.html". The "mm" prefix identifies it as something other than a > set.mm label (labels beginning with "mm" are not allowed by "verify > markup"). > > Norm > > On Monday, November 2, 2020 at 9:47:43 AM UTC-5 [email protected] wrote: > >> Not dead! >> >> Back in July, I mined Frege's original work on triple disjunction and >> conjunction and just last night got them into a PR. >> >> I looked into SVG to reproduce Frege's original notation for the web, and >> created a mmfrege.raw.html to give examples comparing both the notation and >> possible idiomatic translations which use set.mm's wider range of >> notations. Attached is a zip file with the SVG and metamath-processed >> output file mmfrege.html and a PDF. >> >> On Saturday, July 11, 2020 at 9:15:03 AM UTC-7 Norman Megill wrote: >> >>> On Thursday, July 9, 2020 at 4:41:43 PM UTC-4, Richard Penner wrote: >>>> >>>> >>>> NM has stated (can't find where) that he would prefer not move my Frege >>>> sections to the main set.mm. >>>> >>> >>> It was here: >>> https://github.com/metamath/set.mm/pull/1604#issuecomment-618464178 >>> >>> >>> >>>> I think his preference was for partition of hereditary and Frege from >>>> set.mm if the website supported it. Perhaps he may warm to FL's >>>> proposal. I am happy that we got some of the work on transitive closure of >>>> relations into the main section. My November notes on Frege were lengthy >>>> and complex without the t+ function. >>>> >>> >>> My basic objection was that it adds new axioms. set.mm was originally >>> intended to show the derivation of ZFC theorems from a standard set of >>> axioms, and I still think that should be its main purpose. Adding >>> alternative axioms can be confusing and is probably not interesting to >>> someone who just wants to get into the basics of set theory. Yesterday I >>> took out the remaining alternate axioms in the prop/pred calc sections >>> (that really shouldn't have been there) and moved most of them to my >>> mathbox for now. >>> >>> Your work on Frege is very nice. I had mentioned the possibility of a >>> separate .mm file and directory for it, but in addition to the work needed >>> to create the auxiliary files, it wouldn't necessarily be as visible as >>> having it in set.mm (for example new proofs would not show up on set.mm's >>> Most Recent Proofs page). >>> >>> Instead, I have been thinking about putting all alternate >>> axiomatizations at the end of the main part of set.mm (just before the >>> start of mathboxes) in a new section called "Historical and alternate >>> axiomatizations", along the lines of what I think FL had in mind. This >>> will make it impossible for them to be used accidentally in the main part >>> of set.mm,. Accidental use in mathboxes could still happen in >>> principle, but "(New usage is discouraged.)" tags would largely prevent >>> that, and anyway it would quickly be discovered whenever mathbox material >>> is moved into the main part. (We can't add a new section after mathboxes >>> without significant changes to metamath.exe, and anyway I'd rather keep to >>> the simpler idea that mathboxes are at the end of set.mm.) >>> >>> Norm >>> >> -- 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/9a556bd5-1195-4852-be3d-c26a32c2a743n%40googlegroups.com.
