metamath  

Messages by Thread

• • Re: [Metamath] Re: My contribution to Metamath's mmsolitaire project Samiro Discher
• [Metamath] New "collective" contributor ? Benoit
  • Re: [Metamath] New "collective" contributor ? Mario Carneiro
  • Re: [Metamath] New "collective" contributor ? Benoit
• [Metamath] How to display a backquote in a comment ? Benoit
  • Re: [Metamath] How to display a backquote in a comment ? Mario Carneiro
  • Re: [Metamath] How to display a backquote in a comment ? Benoit
• [Metamath] Metamath mirrors: Current state & proposed plan David A. Wheeler
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan Mingli Yuan
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan heiphohmia via Metamath
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan David A. Wheeler
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan Jim Kingdon
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan heiphohmia via Metamath
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan David A. Wheeler
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan David A. Wheeler
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan Cris Perdue
  • Re: [Metamath] Metamath mirrors: Current state & proposed plan David A. Wheeler
• [Metamath] Need help reaching out to one of ypur members Federico Cretella
  • Re: [Metamath] Need help reaching out to one of ypur members Jim Kingdon
• [Metamath] Znnenlem? David Starner
  • [Metamath] Re: Znnenlem? Benoit
  • [Metamath] Re: Znnenlem? 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Znnenlem? Benoit
• [Metamath] Main metamath website generates its own web pages - needs a little slimming David A. Wheeler
  • Re: [Metamath] Main metamath website generates its own web pages - needs a little slimming Jim Kingdon
• [Metamath] Making progress on generating Metamath website without us2.metamath.org David A. Wheeler
  • [Metamath] Plan to start generating Metamath website without us2.metamath.org David A. Wheeler
  • [Metamath] Re: Plan to start generating Metamath website without us2.metamath.org Benoit
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org David A. Wheeler
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org David A. Wheeler
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org Benoit
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org David A. Wheeler
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org David A. Wheeler
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org David A. Wheeler
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org Benoit
  • Re: [Metamath] Plan to start generating Metamath website without us2.metamath.org David A. Wheeler
• [Metamath] Alternative Proofs Antony Bartlett
  • Re: [Metamath] Alternative Proofs David A. Wheeler
  • Re: [Metamath] Alternative Proofs Antony Bartlett
  • Re: [Metamath] Alternative Proofs Benoit
  • Re: [Metamath] Alternative Proofs Antony Bartlett
  • Re: [Metamath] Alternative Proofs 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Alternative Proofs Glauco
  • Re: [Metamath] Alternative Proofs Antony Bartlett
• [Metamath] Proposal: Implement "branch protection" on set.mm GitHub repository branch "develop" David A. Wheeler
  • Re: [Metamath] Proposal: Implement "branch protection" on set.mm GitHub repository branch "develop" Jim Kingdon
  • Re: [Metamath] Proposal: Implement "branch protection" on set.mm GitHub repository branch "develop" Benoit
  • Re: [Metamath] Proposal: Implement "branch protection" on set.mm GitHub repository branch "develop" David A. Wheeler
  • Re: [Metamath] Proposal: Implement "branch protection" on set.mm GitHub repository branch "develop" David A. Wheeler
  • Re: [Metamath] Proposal: Implement "branch protection" on set.mm GitHub repository branch "develop" 'Alexander van der Vekens' via Metamath
• [Metamath] MMJ question [email protected]
  • Re: [Metamath] MMJ question Antony Bartlett
  • Re: [Metamath] MMJ question 'Peter H. Meadows' via Metamath
  • Re: [Metamath] MMJ question Antony Bartlett
  • [Metamath] Re: MMJ question Glauco
  • RE: [Metamath] Re: MMJ question [email protected]
  • Re: [Metamath] Re: MMJ question Mario Carneiro
  • Re: [Metamath] Re: MMJ question Antony Bartlett
  • Re: [Metamath] Re: MMJ question Mario Carneiro
  • Re: [Metamath] Re: MMJ question Glauco
  • Re: [Metamath] Re: MMJ question Antony Bartlett
• [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF) Jim Kingdon
  • Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over I heiphohmia via Metamath
  • Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF) David A. Wheeler
  • Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF) Jim Kingdon
  • Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF) David A. Wheeler
  • Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF) Benoit
  • Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF) David A. Wheeler
  • Re: [Metamath] Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF) Jim Kingdon
• [Metamath] Searching an expression in mmj2 Benoit
  • [Metamath] Re: Searching an expression in mmj2 Glauco
  • [Metamath] Re: Searching an expression in mmj2 Benoit
  • Re: [Metamath] Re: Searching an expression in mmj2 Steven Nguyen
  • Re: [Metamath] Re: Searching an expression in mmj2 Benoit
  • Re: [Metamath] Searching an expression in mmj2 David A. Wheeler
• [Metamath] Metamath site us.metamath.org status and plans David A. Wheeler
  • [Metamath] Re: Metamath site us.metamath.org status and plans Jon P
  • Re: [Metamath] Metamath site us.metamath.org status and plans David A. Wheeler
  • Re: [Metamath] Metamath site us.metamath.org status and plans savask
  • Re: [Metamath] Re: Metamath site us.metamath.org status and plans Jim Kingdon
  • [Metamath] Re: Metamath site us.metamath.org status and plans Glauco
  • Re: [Metamath] Metamath site us.metamath.org status and plans David A. Wheeler
  • Re: [Metamath] Metamath site us.metamath.org status and plans Cris Perdue
  • Re: [Metamath] Metamath site us.metamath.org status and plans David A. Wheeler
  • Re: [Metamath] Metamath site us.metamath.org status and plans Mázsa Péter
  • Re: [Metamath] Metamath site us.metamath.org status and plans Cris Perdue
• [Metamath] Symbol for ordinal number 0 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Symbol for ordinal number 0 Jim Kingdon
  • Re: [Metamath] Symbol for ordinal number 0 savask
  • Re: [Metamath] Symbol for ordinal number 0 Jim Kingdon
  • Re: [Metamath] Symbol for ordinal number 0 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Symbol for ordinal number 0 Benoit
  • Re: [Metamath] Symbol for ordinal number 0 Mario Carneiro
  • Re: [Metamath] Symbol for ordinal number 0 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Symbol for ordinal number 0 Mario Carneiro
  • Re: [Metamath] Symbol for ordinal number 0 'Alexander van der Vekens' via Metamath
• [Metamath] Link to id1 on the metamath website Sophie
  • Re: [Metamath] Link to id1 on the metamath website Jim Kingdon
• [Metamath] Metamath website changes David A. Wheeler
  • Re: [Metamath] Metamath website changes Jim Kingdon
  • Re: [Metamath] Metamath website changes David A. Wheeler
• [Metamath] Proposal: Comment marking for intentionally unused hypothesis/hypotheses David A. Wheeler
  • [Metamath] Re: Proposal: Comment marking for intentionally unused hypothesis/hypotheses 'Alexander van der Vekens' via Metamath
  • Re: [Metamath] Re: Proposal: Comment marking for intentionally unused hypothesis/hypotheses Mario Carneiro
  • Re: [Metamath] Proposal: Comment marking for intentionally unused hypothesis/hypotheses David A. Wheeler
  • Re: [Metamath] Re: Proposal: Comment marking for intentionally unused hypothesis/hypotheses Benoit
  • Re: [Metamath] Re: Proposal: Comment marking for intentionally unused hypothesis/hypotheses Mario Carneiro
  • Re: [Metamath] Proposal: Comment marking for intentionally unused hypothesis/hypotheses David A. Wheeler
  • Re: [Metamath] Proposal: Comment marking for intentionally unused hypothesis/hypotheses savask
• [Metamath] Convention for labels in set.mm: lower case only? 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Convention for labels in set.mm: lower case only? Benoit
• [Metamath] Transcendental numbers and the metamath 100. Jon P
  • [Metamath] Re: Transcendental numbers and the metamath 100. savask
• [Metamath] Finding lemmata which minimize set.mm savask
  • Re: [Metamath] Finding lemmata which minimize set.mm David A. Wheeler
  • [Metamath] Re: Finding lemmata which minimize set.mm 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Finding lemmata which minimize set.mm savask
  • Re: [Metamath] Re: Finding lemmata which minimize set.mm Mario Carneiro
  • [Metamath] Re: Finding lemmata which minimize set.mm 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Finding lemmata which minimize set.mm savask
  • [Metamath] Re: Finding lemmata which minimize set.mm Benoit
  • [Metamath] Re: Finding lemmata which minimize set.mm savask
  • [Metamath] Re: Finding lemmata which minimize set.mm 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Finding lemmata which minimize set.mm Benoit
  • [Metamath] Re: Finding lemmata which minimize set.mm savask
  • [Metamath] Re: Finding lemmata which minimize set.mm Benoit
  • [Metamath] Re: Finding lemmata which minimize set.mm 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: Finding lemmata which minimize set.mm 'Alexander van der Vekens' via Metamath
• [Metamath] Extensionality ax-ext axext Roland Coghetto
  • [Metamath] Re: Extensionality ax-ext axext Benoit
  • Re: [Metamath] Re: Extensionality ax-ext axext Mario Carneiro
  • Re: [Metamath] Re: Extensionality ax-ext axext Roland Coghetto
• [Metamath] How to typeset "K-regular" in comments Benoit
  • [Metamath] Re: How to typeset "K-regular" in comments 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: How to typeset "K-regular" in comments 'Alexander van der Vekens' via Metamath
  • [Metamath] Re: How to typeset "K-regular" in comments Benoit
• [Metamath] metamath GUI/Game in Smalltalk 'Peter Meadows' via Metamath
  • Re: [Metamath] metamath GUI/Game in Smalltalk Jim Kingdon
  • Re: [Metamath] metamath GUI/Game in Smalltalk 'Peter H. Meadows' via Metamath
  • Re: [Metamath] metamath GUI/Game in Smalltalk Jon P
  • Re: [Metamath] metamath GUI/Game in Smalltalk 'Peter H. Meadows' via Metamath
  • Re: [Metamath] metamath GUI/Game in Smalltalk Antony Bartlett
  • Re: [Metamath] metamath GUI/Game in Smalltalk Cris Perdue
  • Re: [Metamath] metamath GUI/Game in Smalltalk 'Peter H. Meadows' via Metamath
  • Re: [Metamath] metamath GUI/Game in Smalltalk Cris Perdue
  • Re: [Metamath] metamath GUI/Game in Smalltalk 'Peter Meadows' via Metamath
  • Re: [Metamath] metamath GUI/Game in Smalltalk Mo Ti
• [Metamath] Metamath Zero dissertation defense Mario Carneiro
  • [Metamath] Re: Metamath Zero dissertation defense Mario Carneiro
  • [Metamath] Re: Metamath Zero dissertation defense Jon P
  • Re: [Metamath] Re: Metamath Zero dissertation defense heiphohmia via Metamath
  • Re: [Metamath] Re: Metamath Zero dissertation defense Mario Carneiro
  • Re: [Metamath] Re: Metamath Zero dissertation defense Thierry Arnoux
  • Re: [Metamath] Re: Metamath Zero dissertation defense Antony Bartlett
  • Re: [Metamath] Metamath Zero dissertation defense David A. Wheeler
  • Re: [Metamath] Metamath Zero dissertation defense OlivierBinda
• [Metamath] How to tell if proof steps are uninteresting. 'Philip White' via Metamath
  • [Metamath] Re: How to tell if proof steps are uninteresting. Benoit
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. 'Philip White' via Metamath
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Mario Carneiro
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Benoit
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Mario Carneiro
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Benoit
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Mario Carneiro
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Benoit
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Mario Carneiro
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Benoit
  • Re: [Metamath] Re: How to tell if proof steps are uninteresting. Mario Carneiro
• [Metamath] New verifiers/parsers/community projects Thierry Arnoux
  • [Metamath] Re: New verifiers/parsers/community projects Benoit
  • Re: [Metamath] Re: New verifiers/parsers/community projects Mario Carneiro
  • Re: [Metamath] Re: New verifiers/parsers/community projects 'Philip White' via Metamath
  • Re: [Metamath] Re: New verifiers/parsers/community projects Mario Carneiro
  • Re: [Metamath] Re: New verifiers/parsers/community projects 'Philip White' via Metamath
  • Re: [Metamath] Re: New verifiers/parsers/community projects Mario Carneiro
  • Re: [Metamath] Re: New verifiers/parsers/community projects Jim Kingdon
  • Re: [Metamath] Re: New verifiers/parsers/community projects Mario Carneiro
  • Re: [Metamath] Re: New verifiers/parsers/community projects Raph Levien
  • Re: [Metamath] Re: New verifiers/parsers/community projects 'Philip White' via Metamath
  • Re: [Metamath] Re: New verifiers/parsers/community projects Jon P
  • Re: [Metamath] Re: New verifiers/parsers/community projects Jim Kingdon
  • Re: [Metamath] Re: New verifiers/parsers/community projects Jon P
  • Re: [Metamath] Re: New verifiers/parsers/community projects Jim Kingdon
  • [Metamath] Re: New verifiers/parsers/community projects Glauco
  • Re: [Metamath] New verifiers/parsers/community projects Antony Bartlett
• [Metamath] Lexing/parsing a Metamath database Benoit
  • Re: [Metamath] Lexing/parsing a Metamath database Mario Carneiro
  • Re: [Metamath] Lexing/parsing a Metamath database Benoit
  • Re: [Metamath] Lexing/parsing a Metamath database Thierry Arnoux
  • Re: [Metamath] Lexing/parsing a Metamath database Mario Carneiro
• [Metamath] checkmm ported to TypeScript Antony Bartlett
  • Re: [Metamath] checkmm ported to TypeScript Thierry Arnoux
  • Re: [Metamath] checkmm ported to TypeScript Mario Carneiro
  • Re: [Metamath] checkmm ported to TypeScript Antony Bartlett
  • Re: [Metamath] checkmm ported to TypeScript Thierry Arnoux
  • Re: [Metamath] checkmm ported to TypeScript Mario Carneiro
  • Re: [Metamath] checkmm ported to TypeScript Antony Bartlett
  • Re: [Metamath] checkmm ported to TypeScript David A. Wheeler
  • Re: [Metamath] checkmm ported to TypeScript Benoit

• Earlier messages
• Later messages