type error_record = {origin_structure : string,
                     origin_function  : string,
                     message          : string}
STRUCTURE
SYNOPSIS
Type abbreviation for HOL exceptions in Feedback module.
DESCRIPTION
The type abbreviation error_record declares the standard format of HOL exceptions. The origin_structure field denotes the module that the exception has been raised in, the origin_function field gives the name of the function the exception has been raised in, and the message field should give an explanation of why the exception has been raised.
SEEALSO
HOL  Kananaskis-10