print_datatypes
EmitTeX.print_datatypes : string -> unit
Prints datatype declarations for the named theory to the screeen (standard out).
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: Restarting 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