Print sharing control

[msaaltink]

This adds an ability to control the threshold that determines when the pretty printer "memoizes" a term (that is, creates a let-bound "x@" variable). As the help string says "Set the number times a subterm must be shared for it to be let-bound in printer output."

My original thought was that I could tweak this to make formulas more readable, but it is really hard to find the right number---too high and the type parameters that appear in terms can obscure the information, too low and there is still too much indirection in the printer output.

It has, however, proven to be useful in the following situation: after some changes to a specification, some proofs break. You can set this number very high, then print_goal in the old proof, and similarly in the new proof, and then use diff on the outputs to get a sense of what's changed. With the memoized variables, typically the whole formula is different, but with the expanded, unmemoized output it is pretty easy to see the differences.

[robdockins]

Seems like a practical approach to me.

[robdockins]

However, regarding finding differences between terms, maybe we should build a specific tool for this sort of thing. We could output two terms of interest into the external format and find some way to let users explore a tree-diff.