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