1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
\DOC delete_user_printer
\TYPE {delete_user_printer : string -> unit}
\SYNOPSIS
Remove user-defined printer from the HOL Light term printing.
\DESCRIBE
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
Never fails, even if there is no printer with the given tag.
\EXAMPLE
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 = ()
}
\SEEALSO
install_user_printer, try_user_printer.
\ENDDOC
|
