Auxiliary files providing glue between a standard HOL installation and what we want to use for CakeML development.
basicComputeLib.sml: Build a basic compset for evaluation in the logic.
induct_tweakLib.sml: Code for adjusting and improving induction theorems.
libScript.sml: Renamnts of Lem dependency
miscScript.sml: Miscellaneous definitions and minor lemmas used throughout the development.
packLib.sml: A library for packing theorems, terms, and types as theorems (which can thereby be saved in theories).
preamble.sml: Proof tools (e.g. tactics) used throughout the development.