Setting tableaux using prooftrees.sty

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 planning to use 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 and beat 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. This will contain some notes on using the package, e.g. on how to avoid it clashing with busstrees.sty, and on any useful undocumented tweaks I find. And then I’ll also give a few examples, including some constructed for IFL.

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!)