----------------------------------------------------------------------
print_datatypes                                              (EmitTeX)
----------------------------------------------------------------------
print_datatypes : string -> unit

SYNOPSIS
Prints datatype declarations for the named theory to the screeen (standard out).

DESCRIBE
An invocation of {print_datatypes thy}, where {thy} is the name of a currently
loaded theory segment, will print the datatype declarations made in that
theory.

FAILURE
Never fails. If {thy} is not the name of a currently loaded theory segment then
no output will be produced.

EXAMPLE

- new_theory "example";
<<HOL message: Created theory "example">>
> val it = () : unit
- val _ = Hol_datatype `example = First | Second`;
<<HOL message: Defined type: "example">>
- EmitTeX.print_datatypes "example";
example = First | Second
> val it = () : unit


SEEALSO
EmitTeX.datatype_thm_to_string, bossLib.Hol_datatype.

----------------------------------------------------------------------