Add a framework for pretty printing
Make the term printer pluggable
Fix printing of lambdas
Make pretty printing less prone to line breaks and indentation

Now there are roughly as many boxes as parentheses and lambda
expressions.
Also use the pretty printer for metaterms
New settable flag "instantiations" to show eigenvariable instantiations

This will let you see what your old eigenvariables turned into
Add a notation for negation

The form

   ~ F

parses as

   F -> false

and the latter prints as the former.