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