Structure RecordType

Source File Identifier index Theory binding index

signature RecordType =
  include Abbrev

  val debugp : bool ref

  val prove_recordtype_thms : TypeBasePure.tyinfo * string list ->

  val update_tyinfo :
      ((string * TypeBase.rcd_fieldinfo) list * thm list * thm list) option ->
      thm list -> TypeBasePure.tyinfo -> TypeBasePure.tyinfo


   [prove_recordtype_thms] takes a tyinfo with the basic information
    about the type and a list of names for the record fields.  Returns
    an augmented tyinfo and a string corresponding to an ML expression
    which modifies a tyinfo in the same way as the result has just been

   [update_tyinfo ths] transforms a tyinfo by adding the ths to it as
    extra simplification theorems. Also updates the tyinfo with
    accessor and update information.


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1