Syntax of the HOL inference system with ad-hoc overloading.

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.

holSyntaxCyclicityScript.sml: Implementation of cyclicity check for function definitions based on Kunčar, CPP 2015

holSyntaxExtraScript.sml: Some lemmas about the syntactic functions.

holSyntaxRenamingScript.sml: Verification of rename_apart: rename_apart r c gives a function f, such that f(r) ∩ c = ∅ , f(r) ∩ r = ∅ and dom(f) = r ∩ c.

holSyntaxRenamingTyvarScript.sml:

• Properties of RenamingTheory for our syntax

holSyntaxScript.sml: Defines the HOL inference system.

holSyntaxSyntax.sml: ML functions for constructing and picking apart terms arising from holSyntaxTheory.