datatype_theorems : string -> (string * thm) list

- STRUCTURE
- 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

HOL Kananaskis-13