1signature ConsThms = 2sig 3 type thm = Thm.thm 4 5 val build : {New_Ty_Existence_Thm : thm, 6 New_Ty_Induct_Thm : thm, 7 New_Ty_Uniqueness_Thm : thm} 8 -> 9 {mutual_constructors_distinct : thm, 10 mutual_constructors_one_one : thm, 11 mutual_cases : thm, 12 argument_extraction_definitions : (string * thm) list} 13 14end 15