Auxiliary definitions used for manipulating (deeply embedded) HOL syntax.
holSyntaxLibScript.sml: Definitions for manipulating (deeply embedded) HOL syntax.
Auxiliary definitions used for manipulating (deeply embedded) HOL syntax.
holSyntaxLibScript.sml: Definitions for manipulating (deeply embedded) HOL syntax.