1signature RecordType = 2sig 3 include Abbrev 4 5 val mk_recordtype_constructor : string -> string 6 7 val prove_recordtype_thms : TypeBasePure.tyinfo * string list -> 8 TypeBasePure.tyinfo 9 10 val update_tyinfo : 11 ((string * TypeBase.rcd_fieldinfo) list * thm list * thm list) option -> 12 thm list -> TypeBasePure.tyinfo -> TypeBasePure.tyinfo 13end 14 15(* 16 17 [prove_recordtype_thms] takes a tyinfo with the basic information 18 about the type and a list of names for the record fields. Returns 19 an augmented tyinfo and a string corresponding to an ML expression 20 which modifies a tyinfo in the same way as the result has just been 21 modified. 22 23 [update_tyinfo ths] transforms a tyinfo by adding the ths to it as 24 extra simplification theorems. Also updates the tyinfo with 25 accessor and update information. 26 27*) 28