Can't speak for anyone else, but for me it was a combination of getting used to the ASCII (at least enough to work with it in mmj2) and using SHOW STATEMENT/ALT_HTML a lot.
Welcome to the project and I'm excited that you have in mind some shortenings which also make things clearer. Those are my favorite kind. On August 2, 2019 12:07:00 PM PDT, Noam Tene <[email protected]> wrote: >Hi, > >I think I can come up with shorter (and more readable) versions for >some of >the proofs I saw on the MPE explorer. >I will never know until I try it. >I would like to try out mmj2 to experiment with some proofs. > >I watched the "Introduction to Metamath & mmj2" ><https://www.youtube.com/watch?v=Rst2hZpWUbU> video mentioned at " >http://us.metamath.org/index.html#faq";. >I looked for the "http://us.metamath.org/index.html#downloads"; section >and >I found: > >mmj2.zip <http://us2.metamath.org:88/ocat/mmj2/mmj2.zip> (7.2 MB) >(latest >version, 2.4.1 26-Jan-2016, maintained by Mario Carneiro) >mmj2-orig.zip <http://us2.metamath.org:88/downloads/mmj2-orig.zip> (Mel > >O'Cat's last official version, 11-Oct-2011) > > >However, a google search for "mmj2 download" came up with something >that >looks like a later version at: >https://groups.google.com/forum/#!topic/metamath/3kN15fc2MdY > >From watching the video, I noticed that mmj2 is a text based editor. >I do not mind ASCII, I even prefer it in some cases. >At the same time, I find the HTML version much easier to read, follow >and >present to newcomers who never heard of Metamath. >Are there any HTML or Lyx based editors that incorporate the mmj2 >features >which I could help beta test? > >Thanks, > >Noam Tene > >-- >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/ee2b8ff7-c648-44b9-96ce-df6066f63cf3%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/D7813D99-39AF-4D97-89E6-3E48EBA7EE40%40panix.com.
