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.