Flag determining whether the assumptions of theorems are printed explicitly.
DESCRIPTION
The reference variable print_all_thm 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.
When it is true, as it is by default, all assumptions of theorems are
printed. When it is false, they are abbreviated by dots.
FAILURE CONDITIONS
Not applicable.
EXAMPLE
# let th = ADD_ASSUM `1 + 1 = 2` (ASSUME `2 + 2 = 4`);;
val th : thm = 2 + 2 = 4, 1 + 1 = 2 |- 2 + 2 = 4
# print_all_thm := false;;
val it : unit = ()
# th;;
val it : thm = ... |- 2 + 2 = 4