[Updated] The first edition of IFL was typeset using FrameMaker (long since defunct on a Mac), so I’m having to LaTeX the second edition from scratch. I’m using Clea Rees’s fairly new package prooftrees.sty for downward-branching tableaux, a.k.a. truth-trees, since this seems to give the right level of control over trees, allows line numbering and line comments, and beats other options by some way.
I have therefore added a link on the LaTeX for Logicians page on tree proofs to a document on setting tableaux using this package [New version 12 Feb] This contains some initial notes on using the package and also gives a few examples.
I’d be very happy to hear about any tips and tricks for this package from other users that could also be shared at LaTeX for Logicians. (And of course, all other suggestions and corrections for L4L are always welcome!)