print_all_thm : bool ref

SYNOPSIS
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

SEE ALSO
pp_print_term, prebroken_binops, print_goal_hyp_max_boxes, print_unambiguous_comprehensions, reverse_interface_mapping, typify_universal_set, unspaced_binops.