type thy_addon
STRUCTURE
SYNOPSIS
Type of theory additions.
DESCRIPTION
The type abbreviation thy_addon, declared as
   type thy_addon = {sig_ps : unit PP.pprinter option,
                     struct_ps : unit PP.pprinter option}
packages up the arguments to adjoin_to_theory. The sig_ps argument is an optional prettyprinter, which will be invoked when the theory signature file is written. The struct_ps argument is an optional prettyprinter invoked when the theory structure file is written.

The unit type parameter in both cases simply means that the pretty-printers won’t be passed any extra information when invoked.

SEEALSO
HOL  Kananaskis-14