Determines which binary operators are line-broken to the left
DESCRIPTION
The reference variable prebroken_binops is one of several settable parameters
controlling printing of terms by pp_print_term, and hence the automatic
printing of terms and theorems at the toplevel. It holds a list of the names of
binary operators that, when a line break is needed, will be printed after the
line break rather than before it. By default it contains just implication.
FAILURE CONDITIONS
Not applicable.
COMMENTS
Putting more operators such as conjunction in this list gives an output format
closer to the one advocated in Lamport's ``How to write a large formula''
paper.