typify_universal_set : bool ref

SYNOPSIS
Determines whether the universe set on a type is printed just as the type.

DESCRIPTION
The reference variable typify_universal_set 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, any universal set UNIV:A->bool (UNIV is a predefined set constant valid over all types) is printed just as (:A). When typify_universal_set is false, it is printed as UNIV, just as for any other constant.

FAILURE CONDITIONS
Not applicable.

EXAMPLE
Note that having this setting is quite useful here:
  # CART_EQ;;
  val it : thm =
    |- !x y. x = y <=> (!i. 1 <= i /\ i <= dimindex (:B) ==> x $ i = y $ i)

USES
HOL Light's Cartesian power type (constructor `^') uses a type to index the power. When this flag is true, formulas often become easier to understand when printed, as in the above example.

SEE ALSO
pp_print_term, prebroken_binops, print_all_thm, print_unambiguous_comprehensions, reverse_interface_mapping, unspaced_binops.