Hi, my first post to this list.
I am trying Metamath. I have a couple of questions about basic whereabouts. 1. is there a way to customize the .tex file you get with a command like : *show proof tfr2 /all /lemmon /tex .* I am getting a .tex file which gives a number of errors when I try to pdflatex it (mostly missing labels) 2. is there a way to output proof in a tree like display (say, sequent calculi / natural deduction style)? 3. is there some kind of IDE for Metamath? Sorry if I am asking questions which have been already asked and answered. Thanks mario -- 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/ee2bb0f9-d530-45d2-8f35-e1d026e67fafn%40googlegroups.com.
