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 : ((string * hol_type) list * thm list * thm list) option -> 11 thm list -> TypeBasePure.tyinfo -> TypeBasePure.tyinfo 12end 13 14(* 15 16 [prove_recordtype_thms] takes a tyinfo with the basic information 17 about the type and a list of names for the record fields. Returns 18 an augmented tyinfo and a string corresponding to an ML expression 19 which modifies a tyinfo in the same way as the result has just been 20 modified. 21 22 [update_tyinfo ths] transforms a tyinfo by adding the ths to it as 23 extra simplification theorems. Also updates the tyinfo with 24 accessor and update information. 25 26*) 27