print_qterm : term -> unit
SYNOPSIS
Prints a HOL term with surrounding quotes to standard output.
DESCRIPTION
The call
print_term tm
prints the usual textual representation of the term
tm
to the standard output, that is
`:tm`
.
FAILURE CONDITIONS
Never fails.
COMMENTS
This is the function that is invoked automatically in the toplevel when printing terms.
SEE ALSO
pp_print_qterm
,
pp_print_term
,
print_term
.