1\DOC
2
3\TYPE {datatype_thm_to_string : thm -> string}
4
5\SYNOPSIS
6Converts a datatype theorem to a string.
7
8\DESCRIBE
9An invocation of {datatype_thm_to_string thm}, where {thm} is a datatype theorem produced by {Hol_datatype}, will return a string that corresponds with the orginal datatype declaration.
10
11\FAILURE
12Will fail if the supplied theorem is not a datatype theorem, as created by {Hol_datatype}.
13
14\EXAMPLE
15{
16- new_theory "example";
17<<HOL message: Created theory "example">>
18> val it = () : unit
19- val _ = Hol_datatype `example = First | Second`;
20<<HOL message: Defined type: "example">>
21- EmitTeX.datatype_thm_to_string (theorem "datatype_example");
22> val it = "example = First | Second" : string
23}
24
25\SEEALSO
26bossLib.Hol_datatype.
27\ENDDOC
28