max_print_depth : int ref
STRUCTURE
Globals
SYNOPSIS
Sets depth bound on prettyprinting.
DESCRIPTION
The reference variable max_print_depth is used to define the maximum depth of printing for the pretty printer. If the number of blocks (an internal notion used by the prettyprinter) becomes greater than the value set by max_print_depth then the blocks are abbreviated by the holophrast .... By default, the value of max_print_depth is ~1. This is interpreted to mean ‘print everything’.
FAILURE
Never fails.
EXAMPLE
To change the maximum depth setting to 10, the command will be: 
   - max_print_depth := 10;
   > val it = () : unit
The theorem numeralTheory.numeral_distrib then prints as follows: 
- numeralTheory.numeral_distrib;
> val it =
    |- (!n. 0 + n = n) /\ (!n. n + 0 = n) /\
       (!n m. NUMERAL n + NUMERAL m = NUMERAL (iZ (n + m))) /\
       (!n. 0 * n = 0) /\ (!n. n * 0 = 0) /\
       (!n m. ... ... * ... ... = NUMERAL (... * ...)) /\
       (!n. ... - ... = 0) /\ (!n. ... = ...) /\ (!... .... ...) /\ ... /\ ...
     : thm

HOL  Kananaskis-14