It becomes more and more difficult to follow this thread, because many different topics are discussed. Maybe it would be a good idea to start new threads (one for each topic: abbreviation of square root, conventions for labels, presentation of tooltips, etc), although they all have their origins in the video of George Hotz...
-- 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/6298d2f1-15a2-4073-bfd0-59afca56a780%40googlegroups.com.
