datatype_theorems : string -> (string * thm) list
STRUCTURE
EmitTeX
SYNOPSIS
All the datatype theorems stored in the named theory.
DESCRIPTION
An invocation datatype_theorems thy, where thy is the name of a currently loaded theory segment, will return a list of the datatype theorems stored in that theory. Each theorem is paired with the name of the datatype in the result. The string "-" may be used to denote the current theory segment.
FAILURE
Never fails. If thy is not the name of a currently loaded theory segment, the empty list is returned.
EXAMPLE
- new_theory "example";
<<HOL message: Created theory "example">>
> val it = () : unit
- val _ = Hol_datatype `example = First | Second`;
<<HOL message: Defined type: "example">>
- EmitTeX.datatype_theorems "example";
> val it = [("example", |- DATATYPE (example First Second))] :
  (string * thm) list
SEEALSO
theorems, Hol_datatype
HOL  Trindemossen-1