delete_user_printer : string -> unit
Remove user-defined printer from the HOL Light term printing.
HOL Light allows arbitrary user printers to be inserted into the toplevel
printer so that they are invoked on all applicable subterms (see
install_user_printer). The call delete_user_printer s removes any such
printer associated with the tag s.
- FAILURE CONDITIONS
Never fails, even if there is no printer with the given tag.
If a user printer has been installed as in the example given for
install_user_printer, it can be removed again by:
# delete_user_printer "print_typed_var";;
val it : unit = ()
- SEE ALSO