- SYNOPSIS
-
Prints a HOL theorem to the standard output.
- DESCRIPTION
-
The call print_thm th prints the usual textual representation of the
theorem th to the standard output.
- COMMENTS
-
This is invoked automatically at the toplevel when theorems are printed.
- SEE ALSO
-
print_type, print_term.