Syntax of the HOL inference system.
holAxiomsSyntaxScript.sml: Context extensions for asserting the mathematical axioms.
holBoolSyntaxScript.sml: Definitions to extend a theory context to include the theory of Booleans, and some basic syntactic properties about these extensions.
holConservativeScript.sml: Functions and proofs about expanding constant definitions.
holSyntaxExtraScript.sml: Some lemmas about the syntactic functions.
holSyntaxScript.sml: Defines the HOL inference system.
holSyntaxSyntax.sml: ML functions for constructing and picking apart terms arising from holSyntaxTheory.