prebroken_binops : string list ref
- SYNOPSIS
-
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.
- SEE ALSO
-
pp_print_term, print_all_thm, print_unambiguous_comprehensions,
reverse_interface_mapping, typify_universal_set, unspaced_binops.